Expression of type Conditional

from the theory of proveit.linear_algebra.tensors

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, K, V, b, i, k
from proveit.core_expr_types import U_1_to_i, W_1_to_k, a_1_to_i, c_1_to_k, d_1_to_i, e_1_to_k
from proveit.linear_algebra import TensorProd, VecSpaces
from proveit.logic import And, Equals, Forall, Implies, InSet
from proveit.numbers import Natural

# build up the expression from sub-expressions
expr = Conditional(Forall(instance_param_or_params = [U_1_to_i, V, W_1_to_k], instance_expr = Forall(instance_param_or_params = [a_1_to_i, c_1_to_k, d_1_to_i, e_1_to_k], instance_expr = Forall(instance_param_or_params = [b], instance_expr = Implies(Equals(TensorProd(a_1_to_i, c_1_to_k), TensorProd(d_1_to_i, e_1_to_k)).with_wrapping_at(2), Equals(TensorProd(a_1_to_i, b, c_1_to_k), TensorProd(d_1_to_i, b, e_1_to_k)).with_wrapping_at(2)).with_wrapping_at(2), domain = V), domains = [U_1_to_i, W_1_to_k, U_1_to_i, W_1_to_k]).with_wrapping(), domain = VecSpaces(K)).with_wrapping(), And(InSet(i, Natural), InSet(k, Natural)))

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_{U_{1}, U_{2}, \ldots, U_{i}, V, W_{1}, W_{2}, \ldots, W_{k} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)}~\\
\left[\begin{array}{l}\forall_{\left(a_{1} \in U_{1}\right), \left(a_{2} \in U_{2}\right), \ldots, \left(a_{i} \in U_{i}\right),\left(c_{1} \in W_{1}\right), \left(c_{2} \in W_{2}\right), \ldots, \left(c_{k} \in W_{k}\right),\left(d_{1} \in U_{1}\right), \left(d_{2} \in U_{2}\right), \ldots, \left(d_{i} \in U_{i}\right),\left(e_{1} \in W_{1}\right), \left(e_{2} \in W_{2}\right), \ldots, \left(e_{k} \in W_{k}\right)}~\\
\left[\forall_{b \in V}~\left(\begin{array}{c} \begin{array}{l} \left(\begin{array}{c} \begin{array}{l} \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i}{\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) =  \\ \left(d_{1} {\otimes}  d_{2} {\otimes}  \ldots {\otimes}  d_{i}{\otimes} e_{1} {\otimes}  e_{2} {\otimes}  \ldots {\otimes}  e_{k}\right) \end{array} \end{array}\right) \Rightarrow  \\ \left(\begin{array}{c} \begin{array}{l} \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i} {\otimes} b{\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) =  \\ \left(d_{1} {\otimes}  d_{2} {\otimes}  \ldots {\otimes}  d_{i} {\otimes} b{\otimes} e_{1} {\otimes}  e_{2} {\otimes}  \ldots {\otimes}  e_{k}\right) \end{array} \end{array}\right) \end{array} \end{array}\right)\right]\end{array}\right]\end{array} \textrm{ if } i \in \mathbb{N} ,  k \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: 34 operand: 5
2	Operation	operator: 36 operands: 4
3	ExprTuple	5
4	ExprTuple	6, 7
5	Lambda	parameters: 8 body: 9
6	Operation	operator: 68 operands: 10
7	Operation	operator: 68 operands: 11
8	ExprTuple	12, 72, 13
9	Conditional	value: 14 condition: 15
10	ExprTuple	97, 16
11	ExprTuple	100, 16
12	ExprRange	lambda_map: 17 start_index: 99 end_index: 97
13	ExprRange	lambda_map: 18 start_index: 99 end_index: 100
14	Operation	operator: 34 operand: 21
15	Operation	operator: 36 operands: 20
16	Literal
17	Lambda	parameter: 110 body: 73
18	Lambda	parameter: 110 body: 74
19	ExprTuple	21
20	ExprTuple	22, 23, 24
21	Lambda	parameters: 25 body: 26
22	ExprRange	lambda_map: 27 start_index: 99 end_index: 97
23	Operation	operator: 39 operands: 28
24	ExprRange	lambda_map: 29 start_index: 99 end_index: 100
25	ExprTuple	89, 90, 91, 93
26	Conditional	value: 30 condition: 31
27	Lambda	parameter: 110 body: 32
28	ExprTuple	72, 46
29	Lambda	parameter: 110 body: 33
30	Operation	operator: 34 operand: 41
31	Operation	operator: 36 operands: 37
32	Operation	operator: 39 operands: 38
33	Operation	operator: 39 operands: 40
34	Literal
35	ExprTuple	41
36	Literal
37	ExprTuple	42, 43, 44, 45
38	ExprTuple	73, 46
39	Literal
40	ExprTuple	74, 46
41	Lambda	parameter: 92 body: 48
42	ExprRange	lambda_map: 49 start_index: 99 end_index: 97
43	ExprRange	lambda_map: 50 start_index: 99 end_index: 100
44	ExprRange	lambda_map: 51 start_index: 99 end_index: 97
45	ExprRange	lambda_map: 52 start_index: 99 end_index: 100
46	Operation	operator: 53 operand: 61
47	ExprTuple	92
48	Conditional	value: 55 condition: 56
49	Lambda	parameter: 110 body: 57
50	Lambda	parameter: 110 body: 58
51	Lambda	parameter: 110 body: 59
52	Lambda	parameter: 110 body: 60
53	Literal
54	ExprTuple	61
55	Operation	operator: 62 operands: 63
56	Operation	operator: 68 operands: 64
57	Operation	operator: 68 operands: 65
58	Operation	operator: 68 operands: 66
59	Operation	operator: 68 operands: 67
60	Operation	operator: 68 operands: 69
61	Variable
62	Literal
63	ExprTuple	70, 71
64	ExprTuple	92, 72
65	ExprTuple	101, 73
66	ExprTuple	102, 74
67	ExprTuple	103, 73
68	Literal
69	ExprTuple	104, 74
70	Operation	operator: 76 operands: 75
71	Operation	operator: 76 operands: 77
72	Variable
73	IndexedVar	variable: 78 index: 110
74	IndexedVar	variable: 79 index: 110
75	ExprTuple	80, 81
76	Literal
77	ExprTuple	82, 83
78	Variable
79	Variable
80	Operation	operator: 87 operands: 84
81	Operation	operator: 87 operands: 85
82	Operation	operator: 87 operands: 86
83	Operation	operator: 87 operands: 88
84	ExprTuple	89, 90
85	ExprTuple	91, 93
86	ExprTuple	89, 92, 90
87	Literal
88	ExprTuple	91, 92, 93
89	ExprRange	lambda_map: 94 start_index: 99 end_index: 97
90	ExprRange	lambda_map: 95 start_index: 99 end_index: 100
91	ExprRange	lambda_map: 96 start_index: 99 end_index: 97
92	Variable
93	ExprRange	lambda_map: 98 start_index: 99 end_index: 100
94	Lambda	parameter: 110 body: 101
95	Lambda	parameter: 110 body: 102
96	Lambda	parameter: 110 body: 103
97	Variable
98	Lambda	parameter: 110 body: 104
99	Literal
100	Variable
101	IndexedVar	variable: 105 index: 110
102	IndexedVar	variable: 106 index: 110
103	IndexedVar	variable: 107 index: 110
104	IndexedVar	variable: 108 index: 110
105	Variable
106	Variable
107	Variable
108	Variable
109	ExprTuple	110
110	Variable