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 Conditional, M, i, n
from proveit.core_expr_types import a_1_to_n, a_i, v_1_to_n, v_i
from proveit.linear_algebra import Adj, Dim, HilbertSpaces, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum
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
from proveit.physics.quantum.algebra import v_1_to_n_kets

# build up the expression from sub-expressions
sub_expr1 = Adj(M)
expr = Conditional(Forall(instance_param_or_params = [M], instance_expr = Iff(Equals(Qmult(sub_expr1, M), Qmult(M, sub_expr1)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n], instance_expr = Equals(M, VecSum(index_or_indices = [i], summand = ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))), domain = Interval(one, n))), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n_kets), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), domain = LinMap(Hspace, Hspace)), 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\{\forall_{M \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)}~\left(\begin{array}{c} \begin{array}{l} \left(\left(M^{\dagger} \thinspace M\right) = \left(M \thinspace M^{\dagger}\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{\left\{\lvert v_{1} \rangle, \lvert v_{2} \rangle, \ldots, \lvert v_{n} \rangle\right\}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n} \in \mathbb{C}}~\\
\left(M = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right)\end{array}\right]\end{array}\right] \end{array} \end{array}\right) \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: 61 operands: 5
3	Literal
4	ExprTuple	6
5	ExprTuple	7, 8
6	Lambda	parameter: 65 body: 9
7	Operation	operator: 10 operands: 11
8	Operation	operator: 59 operands: 12
9	Conditional	value: 13 condition: 14
10	Literal
11	ExprTuple	57, 15
12	ExprTuple	16, 101
13	Operation	operator: 17 operands: 18
14	Operation	operator: 86 operands: 19
15	Literal
16	Operation	operator: 20 operand: 57
17	Literal
18	ExprTuple	21, 22
19	ExprTuple	65, 23
20	Literal
21	Operation	operator: 59 operands: 24
22	Operation	operator: 42 operand: 30
23	Operation	operator: 26 operands: 27
24	ExprTuple	28, 29
25	ExprTuple	30
26	Literal
27	ExprTuple	57, 57
28	Operation	operator: 94 operands: 31
29	Operation	operator: 94 operands: 32
30	Lambda	parameters: 33 body: 34
31	ExprTuple	35, 65
32	ExprTuple	65, 35
33	ExprTuple	36
34	Conditional	value: 37 condition: 38
35	Operation	operator: 39 operand: 65
36	ExprRange	lambda_map: 41 start_index: 100 end_index: 101
37	Operation	operator: 42 operand: 45
38	Operation	operator: 86 operands: 44
39	Literal
40	ExprTuple	65
41	Lambda	parameter: 92 body: 83
42	Literal
43	ExprTuple	45
44	ExprTuple	46, 47
45	Lambda	parameters: 48 body: 49
46	Operation	operator: 63 operand: 56
47	Operation	operator: 51 operand: 57
48	ExprTuple	53
49	Conditional	value: 54 condition: 55
50	ExprTuple	56
51	Literal
52	ExprTuple	57
53	ExprRange	lambda_map: 58 start_index: 100 end_index: 101
54	Operation	operator: 59 operands: 60
55	Operation	operator: 61 operands: 62
56	Operation	operator: 63 operands: 64
57	Variable
58	Lambda	parameter: 92 body: 81
59	Literal
60	ExprTuple	65, 66
61	Literal
62	ExprTuple	67
63	Literal
64	ExprTuple	68
65	Variable
66	Operation	operator: 69 operand: 73
67	ExprRange	lambda_map: 71 start_index: 100 end_index: 101
68	ExprRange	lambda_map: 72 start_index: 100 end_index: 101
69	Literal
70	ExprTuple	73
71	Lambda	parameter: 92 body: 74
72	Lambda	parameter: 92 body: 75
73	Lambda	parameter: 108 body: 76
74	Operation	operator: 86 operands: 77
75	Operation	operator: 102 operand: 83
76	Conditional	value: 79 condition: 80
77	ExprTuple	81, 82
78	ExprTuple	83
79	Operation	operator: 84 operands: 85
80	Operation	operator: 86 operands: 87
81	IndexedVar	variable: 93 index: 92
82	Literal
83	IndexedVar	variable: 106 index: 92
84	Literal
85	ExprTuple	89, 90
86	Literal
87	ExprTuple	108, 91
88	ExprTuple	92
89	IndexedVar	variable: 93 index: 108
90	Operation	operator: 94 operands: 95
91	Operation	operator: 96 operands: 97
92	Variable
93	Variable
94	Literal
95	ExprTuple	98, 99
96	Literal
97	ExprTuple	100, 101
98	Operation	operator: 102 operand: 105
99	Operation	operator: 103 operand: 105
100	Literal
101	Variable
102	Literal
103	Literal
104	ExprTuple	105
105	IndexedVar	variable: 106 index: 108
106	Variable
107	ExprTuple	108
108	Variable