Expression of type Conditional

from the theory of proveit.physics.quantum.algebra

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import A, B, Conditional, i, n
from proveit.core_expr_types import a_1_to_n, a_i, b_1_to_n, b_i, v_1_to_n, v_i
from proveit.linear_algebra import Adj, Commutator, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, Equals, Exists, Iff, InSet, Set
from proveit.numbers import Complex, Interval, one
from proveit.physics.quantum import Bra, Ket, Qmult

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = LinMap(Hspace, Hspace)
sub_expr3 = Interval(one, n)
sub_expr4 = Qmult(Ket(v_i), Bra(v_i))
expr = Conditional(Iff(Equals(Commutator(A, B), VecZero(sub_expr2)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n, b_1_to_n], instance_expr = And(Equals(A, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr4), domain = sub_expr3)), Equals(B, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(b_i, sub_expr4), domain = sub_expr3))).with_wrapping_at(2), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), And(InSet(A, sub_expr2), InSet(B, sub_expr2), Equals(Adj(A), A), Equals(Adj(B), B)))

expr:

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left\{\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{v_{1}, v_{2}, \ldots, v_{n}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n}, b_{1}, b_{2}, \ldots, b_{n} \in \mathbb{C}}~\\
\left(\begin{array}{c} \left(A = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \land  \\ \left(B = \left(\sum_{i=1}^{n} \left(b_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \end{array}\right)\end{array}\right]\end{array}\right] \end{array} \end{array} \textrm{ if } A \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right) ,  B \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right) ,  A^{\dagger} = A ,  B^{\dagger} = B\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Conditional	value: 1 condition: 2
1	Operation	operator: 3 operands: 4
2	Operation	operator: 57 operands: 5
3	Literal
4	ExprTuple	6, 7
5	ExprTuple	8, 9, 10, 11
6	Operation	operator: 66 operands: 12
7	Operation	operator: 36 operand: 20
8	Operation	operator: 96 operands: 14
9	Operation	operator: 96 operands: 15
10	Operation	operator: 66 operands: 16
11	Operation	operator: 66 operands: 17
12	ExprTuple	18, 19
13	ExprTuple	20
14	ExprTuple	70, 31
15	ExprTuple	72, 31
16	ExprTuple	21, 70
17	ExprTuple	22, 72
18	Operation	operator: 23 operands: 24
19	Operation	operator: 25 operand: 31
20	Lambda	parameters: 45 body: 27
21	Operation	operator: 29 operand: 70
22	Operation	operator: 29 operand: 72
23	Literal
24	ExprTuple	70, 72
25	Literal
26	ExprTuple	31
27	Conditional	value: 32 condition: 33
28	ExprTuple	70
29	Literal
30	ExprTuple	72
31	Operation	operator: 34 operands: 35
32	Operation	operator: 36 operand: 39
33	Operation	operator: 96 operands: 38
34	Literal
35	ExprTuple	53, 53
36	Literal
37	ExprTuple	39
38	ExprTuple	40, 41
39	Lambda	parameters: 42 body: 43
40	Operation	operator: 44 operands: 45
41	Operation	operator: 46 operand: 53
42	ExprTuple	48, 49
43	Conditional	value: 50 condition: 51
44	Literal
45	ExprTuple	52
46	Literal
47	ExprTuple	53
48	ExprRange	lambda_map: 54 start_index: 110 end_index: 111
49	ExprRange	lambda_map: 55 start_index: 110 end_index: 111
50	Operation	operator: 57 operands: 56
51	Operation	operator: 57 operands: 58
52	ExprRange	lambda_map: 59 start_index: 110 end_index: 111
53	Variable
54	Lambda	parameter: 92 body: 83
55	Lambda	parameter: 92 body: 84
56	ExprTuple	60, 61
57	Literal
58	ExprTuple	62, 63
59	Lambda	parameter: 92 body: 64
60	Operation	operator: 66 operands: 65
61	Operation	operator: 66 operands: 67
62	ExprRange	lambda_map: 68 start_index: 110 end_index: 111
63	ExprRange	lambda_map: 69 start_index: 110 end_index: 111
64	IndexedVar	variable: 116 index: 92
65	ExprTuple	70, 71
66	Literal
67	ExprTuple	72, 73
68	Lambda	parameter: 92 body: 74
69	Lambda	parameter: 92 body: 75
70	Variable
71	Operation	operator: 77 operand: 81
72	Variable
73	Operation	operator: 77 operand: 82
74	Operation	operator: 96 operands: 79
75	Operation	operator: 96 operands: 80
76	ExprTuple	81
77	Literal
78	ExprTuple	82
79	ExprTuple	83, 85
80	ExprTuple	84, 85
81	Lambda	parameter: 118 body: 86
82	Lambda	parameter: 118 body: 87
83	IndexedVar	variable: 102 index: 92
84	IndexedVar	variable: 103 index: 92
85	Literal
86	Conditional	value: 89 condition: 91
87	Conditional	value: 90 condition: 91
88	ExprTuple	92
89	Operation	operator: 94 operands: 93
90	Operation	operator: 94 operands: 95
91	Operation	operator: 96 operands: 97
92	Variable
93	ExprTuple	98, 100
94	Literal
95	ExprTuple	99, 100
96	Literal
97	ExprTuple	118, 101
98	IndexedVar	variable: 102 index: 118
99	IndexedVar	variable: 103 index: 118
100	Operation	operator: 104 operands: 105
101	Operation	operator: 106 operands: 107
102	Variable
103	Variable
104	Literal
105	ExprTuple	108, 109
106	Literal
107	ExprTuple	110, 111
108	Operation	operator: 112 operand: 115
109	Operation	operator: 113 operand: 115
110	Literal
111	Variable
112	Literal
113	Literal
114	ExprTuple	115
115	IndexedVar	variable: 116 index: 118
116	Variable
117	ExprTuple	118
118	Variable