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, Dim, HilbertSpaces, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, Equals, Exists, Forall, Iff, InSet, Set
from proveit.numbers import Complex, Interval, NaturalPos, 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(Forall(instance_param_or_params = [Hspace], instance_expr = Forall(instance_param_or_params = [A, B], instance_expr = 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), domain = sub_expr2, conditions = [Equals(Adj(A), A), Equals(Adj(B), B)]).with_wrapping(), domain = HilbertSpaces, condition = Equals(Dim(Hspace), n)).with_wrapping(), InSet(n, NaturalPos))

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}{l}\forall_{\mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}~|~\textrm{Dim}\left(\mathcal{H}\right) = n}~\\
\left[\begin{array}{l}\forall_{A, B \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)~|~A^{\dagger} = A, B^{\dagger} = B}~\\
\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}\right)\end{array}\right]\end{array} \textrm{ if } n \in \mathbb{N}^+\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: 10 operand: 5
2	Operation	operator: 118 operands: 4
3	ExprTuple	5
4	ExprTuple	133, 6
5	Lambda	parameter: 75 body: 7
6	Literal
7	Conditional	value: 8 condition: 9
8	Operation	operator: 10 operand: 13
9	Operation	operator: 79 operands: 12
10	Literal
11	ExprTuple	13
12	ExprTuple	14, 15
13	Lambda	parameters: 46 body: 16
14	Operation	operator: 17 operands: 18
15	Operation	operator: 88 operands: 19
16	Conditional	value: 20 condition: 21
17	Literal
18	ExprTuple	75, 22
19	ExprTuple	23, 133
20	Operation	operator: 24 operands: 25
21	Operation	operator: 79 operands: 26
22	Literal
23	Operation	operator: 27 operand: 75
24	Literal
25	ExprTuple	28, 29
26	ExprTuple	30, 31, 32, 33
27	Literal
28	Operation	operator: 88 operands: 34
29	Operation	operator: 58 operand: 42
30	Operation	operator: 118 operands: 36
31	Operation	operator: 118 operands: 37
32	Operation	operator: 88 operands: 38
33	Operation	operator: 88 operands: 39
34	ExprTuple	40, 41
35	ExprTuple	42
36	ExprTuple	92, 53
37	ExprTuple	94, 53
38	ExprTuple	43, 92
39	ExprTuple	44, 94
40	Operation	operator: 45 operands: 46
41	Operation	operator: 47 operand: 53
42	Lambda	parameters: 67 body: 49
43	Operation	operator: 51 operand: 92
44	Operation	operator: 51 operand: 94
45	Literal
46	ExprTuple	92, 94
47	Literal
48	ExprTuple	53
49	Conditional	value: 54 condition: 55
50	ExprTuple	92
51	Literal
52	ExprTuple	94
53	Operation	operator: 56 operands: 57
54	Operation	operator: 58 operand: 61
55	Operation	operator: 118 operands: 60
56	Literal
57	ExprTuple	75, 75
58	Literal
59	ExprTuple	61
60	ExprTuple	62, 63
61	Lambda	parameters: 64 body: 65
62	Operation	operator: 66 operands: 67
63	Operation	operator: 68 operand: 75
64	ExprTuple	70, 71
65	Conditional	value: 72 condition: 73
66	Literal
67	ExprTuple	74
68	Literal
69	ExprTuple	75
70	ExprRange	lambda_map: 76 start_index: 132 end_index: 133
71	ExprRange	lambda_map: 77 start_index: 132 end_index: 133
72	Operation	operator: 79 operands: 78
73	Operation	operator: 79 operands: 80
74	ExprRange	lambda_map: 81 start_index: 132 end_index: 133
75	Variable
76	Lambda	parameter: 114 body: 105
77	Lambda	parameter: 114 body: 106
78	ExprTuple	82, 83
79	Literal
80	ExprTuple	84, 85
81	Lambda	parameter: 114 body: 86
82	Operation	operator: 88 operands: 87
83	Operation	operator: 88 operands: 89
84	ExprRange	lambda_map: 90 start_index: 132 end_index: 133
85	ExprRange	lambda_map: 91 start_index: 132 end_index: 133
86	IndexedVar	variable: 138 index: 114
87	ExprTuple	92, 93
88	Literal
89	ExprTuple	94, 95
90	Lambda	parameter: 114 body: 96
91	Lambda	parameter: 114 body: 97
92	Variable
93	Operation	operator: 99 operand: 103
94	Variable
95	Operation	operator: 99 operand: 104
96	Operation	operator: 118 operands: 101
97	Operation	operator: 118 operands: 102
98	ExprTuple	103
99	Literal
100	ExprTuple	104
101	ExprTuple	105, 107
102	ExprTuple	106, 107
103	Lambda	parameter: 140 body: 108
104	Lambda	parameter: 140 body: 109
105	IndexedVar	variable: 124 index: 114
106	IndexedVar	variable: 125 index: 114
107	Literal
108	Conditional	value: 111 condition: 113
109	Conditional	value: 112 condition: 113
110	ExprTuple	114
111	Operation	operator: 116 operands: 115
112	Operation	operator: 116 operands: 117
113	Operation	operator: 118 operands: 119
114	Variable
115	ExprTuple	120, 122
116	Literal
117	ExprTuple	121, 122
118	Literal
119	ExprTuple	140, 123
120	IndexedVar	variable: 124 index: 140
121	IndexedVar	variable: 125 index: 140
122	Operation	operator: 126 operands: 127
123	Operation	operator: 128 operands: 129
124	Variable
125	Variable
126	Literal
127	ExprTuple	130, 131
128	Literal
129	ExprTuple	132, 133
130	Operation	operator: 134 operand: 137
131	Operation	operator: 135 operand: 137
132	Literal
133	Variable
134	Literal
135	Literal
136	ExprTuple	137
137	IndexedVar	variable: 138 index: 140
138	Variable
139	ExprTuple	140
140	Variable