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, 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 = MatrixSpace(field = Complex, rows = n, columns = n)
sub_expr3 = Interval(one, n)
sub_expr4 = Qmult(Ket(v_i), Bra(v_i))
expr = 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(CartExp(Complex, n)))).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\{\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} \textrm{ if } A \in \mathbb{C}^{n \times n} ,  B \in \mathbb{C}^{n \times n} ,  A^{\dagger} = A ,  B^{\dagger} = B\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 operands: 4
2	Operation	operator: 57 operands: 5
3	Literal
4	ExprTuple	6, 7
5	ExprTuple	8, 9, 10, 11
6	Operation	operator: 68 operands: 12
7	Operation	operator: 36 operand: 20
8	Operation	operator: 98 operands: 14
9	Operation	operator: 98 operands: 15
10	Operation	operator: 68 operands: 16
11	Operation	operator: 68 operands: 17
12	ExprTuple	18, 19
13	ExprTuple	20
14	ExprTuple	72, 31
15	ExprTuple	74, 31
16	ExprTuple	21, 72
17	ExprTuple	22, 74
18	Operation	operator: 23 operands: 24
19	Operation	operator: 25 operand: 31
20	Lambda	parameters: 45 body: 27
21	Operation	operator: 29 operand: 72
22	Operation	operator: 29 operand: 74
23	Literal
24	ExprTuple	72, 74
25	Literal
26	ExprTuple	31
27	Conditional	value: 32 condition: 33
28	ExprTuple	72
29	Literal
30	ExprTuple	74
31	Operation	operator: 34 operands: 35
32	Operation	operator: 36 operand: 39
33	Operation	operator: 98 operands: 38
34	Literal
35	NamedExprs	field: 87 rows: 113 columns: 113
36	Literal
37	ExprTuple	39
38	ExprTuple	40, 41
39	Lambda	parameters: 42 body: 43
40	Operation	operator: 44 operands: 45
41	Operation	operator: 46 operand: 53
42	ExprTuple	48, 49
43	Conditional	value: 50 condition: 51
44	Literal
45	ExprTuple	52
46	Literal
47	ExprTuple	53
48	ExprRange	lambda_map: 54 start_index: 112 end_index: 113
49	ExprRange	lambda_map: 55 start_index: 112 end_index: 113
50	Operation	operator: 57 operands: 56
51	Operation	operator: 57 operands: 58
52	ExprRange	lambda_map: 59 start_index: 112 end_index: 113
53	Operation	operator: 60 operands: 61
54	Lambda	parameter: 94 body: 85
55	Lambda	parameter: 94 body: 86
56	ExprTuple	62, 63
57	Literal
58	ExprTuple	64, 65
59	Lambda	parameter: 94 body: 66
60	Literal
61	ExprTuple	87, 113
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