Expression of type ExprTuple

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, ExprTuple, Lambda, 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 = ExprTuple(Lambda([A, B], 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(\left(A, B\right) \mapsto \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..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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