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, 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 = 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\{\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..

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