df-st - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-st 10139

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 8831	. 2
2		cch 8798	. . . . . 6
3		cr 5233	. . . . . 6
4		vf	. . . . . . 7
5	4	cv 955	. . . . . 6
6	2, 3, 5	wf 3178	. . . . 5
7		cc0 5234	. . . . . . . 8
8		vx	. . . . . . . . . 10
9	8	cv 955	. . . . . . . . 9
10	9, 5	cfv 3182	. . . . . . . 8
11		cle 5295	. . . . . . . 8
12	7, 10, 11	wbr 2619	. . . . . . 7
13		c1 5235	. . . . . . . 8
14	10, 13, 11	wbr 2619	. . . . . . 7
15	12, 14	wa 223	. . . . . 6 $/\$
16	15, 8, 2	wral 1645	. . . . 5 $/\$
17	6, 16	wa 223	. . . 4 $/\$ $/\$
18		chil 8788	. . . . . . 7
19	18, 5	cfv 3182	. . . . . 6
20	19, 13	wceq 956	. . . . 5
21		vy	. . . . . . . . . . 11
22	21	cv 955	. . . . . . . . . 10
23		cort 8799	. . . . . . . . . 10
24	22, 23	cfv 3182	. . . . . . . . 9
25	9, 24	wss 2047	. . . . . . . 8
26		chj 8802	. . . . . . . . . . 11
27	9, 22, 26	co 3963	. . . . . . . . . 10
28	27, 5	cfv 3182	. . . . . . . . 9
29	22, 5	cfv 3182	. . . . . . . . . 10
30		caddc 5237	. . . . . . . . . 10
31	10, 29, 30	co 3963	. . . . . . . . 9
32	28, 31	wceq 956	. . . . . . . 8
33	25, 32	wi 3	. . . . . . 7
34	33, 21, 2	wral 1645	. . . . . 6
35	34, 8, 2	wral 1645	. . . . 5
36	20, 35	wa 223	. . . 4 $/\$
37	17, 36	wa 223	. . 3 $/\$ $/\$ $/\$ $/\$
38	37, 4	cab 1463	. 2 $/\$ $/\$ $/\$ $/\$
39	1, 38	wceq 956	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

This definition is referenced by: stelt 10141