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, InClass, 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(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(), And(InClass(Hspace, HilbertSpaces), Equals(Dim(Hspace), n)))

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