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, U, i, j, n
from proveit.core_expr_types import v_1_to_n, v_i, v_j
from proveit.linear_algebra import Adj, MatrixSpace, OrthoNormBases, Unitary
from proveit.logic import CartExp, Equals, Forall, Implies, InSet, Set
from proveit.numbers import Complex, Interval, KroneckerDelta, 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
expr = Conditional(Forall(instance_param_or_params = [v_1_to_n], instance_expr = Implies(Forall(instance_param_or_params = [i, j], instance_expr = Equals(Qmult(Bra(v_i), Adj(U), U, Ket(v_j)), KroneckerDelta(i, j)), domain = Interval(one, n)), InSet(U, Unitary(n))), condition = InSet(Set(v_1_to_n_kets), OrthoNormBases(CartExp(Complex, n)))).with_wrapping(), InSet(U, MatrixSpace(field = Complex, rows = n, columns = 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\{\begin{array}{l}\forall_{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(\mathbb{C}^{n}\right)}~\\
\left(\left[\forall_{i, j \in \{1~\ldotp \ldotp~n\}}~\left(\left(\langle v_{i} \rvert \thinspace U^{\dagger} \thinspace U \thinspace \lvert v_{j} \rangle\right) = \delta_{i, j}\right)\right] \Rightarrow \left(U \in \textrm{U}\left(n\right)\right)\right)\end{array} \textrm{ if } U \in \mathbb{C}^{n \times 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: 22 operand: 5
2	Operation	operator: 58 operands: 4
3	ExprTuple	5
4	ExprTuple	76, 6
5	Lambda	parameters: 7 body: 8
6	Operation	operator: 9 operands: 10
7	ExprTuple	11
8	Conditional	value: 12 condition: 13
9	Literal
10	NamedExprs	field: 42 rows: 79 columns: 79
11	ExprRange	lambda_map: 14 start_index: 78 end_index: 79
12	Operation	operator: 15 operands: 16
13	Operation	operator: 58 operands: 17
14	Lambda	parameter: 80 body: 65
15	Literal
16	ExprTuple	18, 19
17	ExprTuple	20, 21
18	Operation	operator: 22 operand: 28
19	Operation	operator: 58 operands: 24
20	Operation	operator: 35 operand: 30
21	Operation	operator: 26 operand: 31
22	Literal
23	ExprTuple	28
24	ExprTuple	76, 29
25	ExprTuple	30
26	Literal
27	ExprTuple	31
28	Lambda	parameters: 56 body: 32
29	Operation	operator: 33 operand: 79
30	Operation	operator: 35 operands: 36
31	Operation	operator: 37 operands: 38
32	Conditional	value: 39 condition: 40
33	Literal
34	ExprTuple	79
35	Literal
36	ExprTuple	41
37	Literal
38	ExprTuple	42, 79
39	Operation	operator: 43 operands: 44
40	Operation	operator: 45 operands: 46
41	ExprRange	lambda_map: 47 start_index: 78 end_index: 79
42	Literal
43	Literal
44	ExprTuple	48, 49
45	Literal
46	ExprTuple	50, 51
47	Lambda	parameter: 80 body: 52
48	Operation	operator: 53 operands: 54
49	Operation	operator: 55 operands: 56
50	Operation	operator: 58 operands: 57
51	Operation	operator: 58 operands: 59
52	Operation	operator: 70 operand: 65
53	Literal
54	ExprTuple	61, 62, 76, 63
55	Literal
56	ExprTuple	84, 85
57	ExprTuple	84, 64
58	Literal
59	ExprTuple	85, 64
60	ExprTuple	65
61	Operation	operator: 66 operand: 75
62	Operation	operator: 68 operand: 76
63	Operation	operator: 70 operand: 77
64	Operation	operator: 72 operands: 73
65	IndexedVar	variable: 82 index: 80
66	Literal
67	ExprTuple	75
68	Literal
69	ExprTuple	76
70	Literal
71	ExprTuple	77
72	Literal
73	ExprTuple	78, 79
74	ExprTuple	80
75	IndexedVar	variable: 82 index: 84
76	Variable
77	IndexedVar	variable: 82 index: 85
78	Literal
79	Variable
80	Variable
81	ExprTuple	84
82	Variable
83	ExprTuple	85
84	Variable
85	Variable