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, MatrixSpace, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, CartExp, 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 = MatrixSpace(field = Complex, rows = n, columns = n)
sub_expr3 = Interval(one, n)
sub_expr4 = Qmult(Ket(v_i), Bra(v_i))
expr = ExprTuple(Lambda(n, 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(CartExp(Complex, n)))).with_wrapping()).with_wrapping_at(2), domain = sub_expr2, conditions = [Equals(Adj(A), A), Equals(Adj(B), B)]).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(n \mapsto \left\{\begin{array}{l}\forall_{A, B \in \mathbb{C}^{n \times n}~|~A^{\dagger} = A, B^{\dagger} = B}~\\
\left(\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathbb{C}^{n \times n}\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(\mathbb{C}^{n}\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 } n \in \mathbb{N}^+\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	parameter: 124 body: 3
2	ExprTuple	124
3	Conditional	value: 4 condition: 5
4	Operation	operator: 6 operand: 9
5	Operation	operator: 109 operands: 8
6	Literal
7	ExprTuple	9
8	ExprTuple	124, 10
9	Lambda	parameters: 35 body: 11
10	Literal
11	Conditional	value: 12 condition: 13
12	Operation	operator: 14 operands: 15
13	Operation	operator: 68 operands: 16
14	Literal
15	ExprTuple	17, 18
16	ExprTuple	19, 20, 21, 22
17	Operation	operator: 79 operands: 23
18	Operation	operator: 47 operand: 31
19	Operation	operator: 109 operands: 25
20	Operation	operator: 109 operands: 26
21	Operation	operator: 79 operands: 27
22	Operation	operator: 79 operands: 28
23	ExprTuple	29, 30
24	ExprTuple	31
25	ExprTuple	83, 42
26	ExprTuple	85, 42
27	ExprTuple	32, 83
28	ExprTuple	33, 85
29	Operation	operator: 34 operands: 35
30	Operation	operator: 36 operand: 42
31	Lambda	parameters: 56 body: 38
32	Operation	operator: 40 operand: 83
33	Operation	operator: 40 operand: 85
34	Literal
35	ExprTuple	83, 85
36	Literal
37	ExprTuple	42
38	Conditional	value: 43 condition: 44
39	ExprTuple	83
40	Literal
41	ExprTuple	85
42	Operation	operator: 45 operands: 46
43	Operation	operator: 47 operand: 50
44	Operation	operator: 109 operands: 49
45	Literal
46	NamedExprs	field: 98 rows: 124 columns: 124
47	Literal
48	ExprTuple	50
49	ExprTuple	51, 52
50	Lambda	parameters: 53 body: 54
51	Operation	operator: 55 operands: 56
52	Operation	operator: 57 operand: 64
53	ExprTuple	59, 60
54	Conditional	value: 61 condition: 62
55	Literal
56	ExprTuple	63
57	Literal
58	ExprTuple	64
59	ExprRange	lambda_map: 65 start_index: 123 end_index: 124
60	ExprRange	lambda_map: 66 start_index: 123 end_index: 124
61	Operation	operator: 68 operands: 67
62	Operation	operator: 68 operands: 69
63	ExprRange	lambda_map: 70 start_index: 123 end_index: 124
64	Operation	operator: 71 operands: 72
65	Lambda	parameter: 105 body: 96
66	Lambda	parameter: 105 body: 97
67	ExprTuple	73, 74
68	Literal
69	ExprTuple	75, 76
70	Lambda	parameter: 105 body: 77
71	Literal
72	ExprTuple	98, 124
73	Operation	operator: 79 operands: 78
74	Operation	operator: 79 operands: 80
75	ExprRange	lambda_map: 81 start_index: 123 end_index: 124
76	ExprRange	lambda_map: 82 start_index: 123 end_index: 124
77	IndexedVar	variable: 129 index: 105
78	ExprTuple	83, 84
79	Literal
80	ExprTuple	85, 86
81	Lambda	parameter: 105 body: 87
82	Lambda	parameter: 105 body: 88
83	Variable
84	Operation	operator: 90 operand: 94
85	Variable
86	Operation	operator: 90 operand: 95
87	Operation	operator: 109 operands: 92
88	Operation	operator: 109 operands: 93
89	ExprTuple	94
90	Literal
91	ExprTuple	95
92	ExprTuple	96, 98
93	ExprTuple	97, 98
94	Lambda	parameter: 131 body: 99
95	Lambda	parameter: 131 body: 100
96	IndexedVar	variable: 115 index: 105
97	IndexedVar	variable: 116 index: 105
98	Literal
99	Conditional	value: 102 condition: 104
100	Conditional	value: 103 condition: 104
101	ExprTuple	105
102	Operation	operator: 107 operands: 106
103	Operation	operator: 107 operands: 108
104	Operation	operator: 109 operands: 110
105	Variable
106	ExprTuple	111, 113
107	Literal
108	ExprTuple	112, 113
109	Literal
110	ExprTuple	131, 114
111	IndexedVar	variable: 115 index: 131
112	IndexedVar	variable: 116 index: 131
113	Operation	operator: 117 operands: 118
114	Operation	operator: 119 operands: 120
115	Variable
116	Variable
117	Literal
118	ExprTuple	121, 122
119	Literal
120	ExprTuple	123, 124
121	Operation	operator: 125 operand: 128
122	Operation	operator: 126 operand: 128
123	Literal
124	Variable
125	Literal
126	Literal
127	ExprTuple	128
128	IndexedVar	variable: 129 index: 131
129	Variable
130	ExprTuple	131
131	Variable