df-st - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-st 10263

Description: Define the set of states on a Hilbert lattice. Definition of [Kalmbach] p. 266.

**Assertion**
Ref	Expression
df-st	$/\$ $/\$ $/\$ $/\$

**Detailed syntax breakdown of Definition df-st**
Step	Hyp	Ref	Expression
1		cst 9011	. 2
2		cch 8978	. . . . . 6
3		cr 5156	. . . . . 6
4		vf	. . . . . . 7
5	4	cv 1098	. . . . . 6
6	2, 3, 5	wf 3141	. . . . 5
7		cc0 5157	. . . . . . . 8
8		vx	. . . . . . . . . 10
9	8	cv 1098	. . . . . . . . 9
10	9, 5	cfv 3145	. . . . . . . 8
11		cle 5218	. . . . . . . 8
12	7, 10, 11	wbr 2587	. . . . . . 7
13		c1 5158	. . . . . . . 8
14	10, 13, 11	wbr 2587	. . . . . . 7
15	12, 14	wa 223	. . . . . 6 $/\$
16	15, 8, 2	wral 1621	. . . . 5 $/\$
17	6, 16	wa 223	. . . 4 $/\$ $/\$
18		chil 8968	. . . . . . 7
19	18, 5	cfv 3145	. . . . . 6
20	19, 13	wceq 1099	. . . . 5
21		vy	. . . . . . . . . . 11
22	21	cv 1098	. . . . . . . . . 10
23		cort 8979	. . . . . . . . . 10
24	22, 23	cfv 3145	. . . . . . . . 9
25	9, 24	wss 2018	. . . . . . . 8
26		chj 8982	. . . . . . . . . . 11
27	9, 22, 26	co 3902	. . . . . . . . . 10
28	27, 5	cfv 3145	. . . . . . . . 9
29	22, 5	cfv 3145	. . . . . . . . . 10
30		caddc 5160	. . . . . . . . . 10
31	10, 29, 30	co 3902	. . . . . . . . 9
32	28, 31	wceq 1099	. . . . . . . 8
33	25, 32	wi 3	. . . . . . 7
34	33, 21, 2	wral 1621	. . . . . 6
35	34, 8, 2	wral 1621	. . . . 5
36	20, 35	wa 223	. . . 4 $/\$
37	17, 36	wa 223	. . 3 $/\$ $/\$ $/\$ $/\$
38	37, 4	cab 1440	. 2 $/\$ $/\$ $/\$ $/\$
39	1, 38	wceq 1099	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

This definition is referenced by: stelt 10265