df-hst - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > df-hst		Structured version Visualization version Unicode version

Definition df-hst 29071

Description: Define the set of complex Hilbert-space-valued states on a Hilbert lattice. Definition of CH-states in [Mayet3] p. 9. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)

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

Distinct variable group:

**Detailed syntax breakdown of Definition df-hst**
Step	Hyp	Ref	Expression
1		chst 27820	. 2
2		chil 27776	. . . . . . 7
3		vf	. . . . . . . 8
4	3	cv 1482	. . . . . . 7
5	2, 4	cfv 5888	. . . . . 6
6		cno 27780	. . . . . 6
7	5, 6	cfv 5888	. . . . 5
8		c1 9937	. . . . 5
9	7, 8	wceq 1483	. . . 4
10		vx	. . . . . . . . 9
11	10	cv 1482	. . . . . . . 8
12		vy	. . . . . . . . . 10
13	12	cv 1482	. . . . . . . . 9
14		cort 27787	. . . . . . . . 9
15	13, 14	cfv 5888	. . . . . . . 8
16	11, 15	wss 3574	. . . . . . 7
17	11, 4	cfv 5888	. . . . . . . . . 10
18	13, 4	cfv 5888	. . . . . . . . . 10
19		csp 27779	. . . . . . . . . 10
20	17, 18, 19	co 6650	. . . . . . . . 9
21		cc0 9936	. . . . . . . . 9
22	20, 21	wceq 1483	. . . . . . . 8
23		chj 27790	. . . . . . . . . . 11
24	11, 13, 23	co 6650	. . . . . . . . . 10
25	24, 4	cfv 5888	. . . . . . . . 9
26		cva 27777	. . . . . . . . . 10
27	17, 18, 26	co 6650	. . . . . . . . 9
28	25, 27	wceq 1483	. . . . . . . 8
29	22, 28	wa 384	. . . . . . 7 $/\$
30	16, 29	wi 4	. . . . . 6 $/\$
31		cch 27786	. . . . . 6
32	30, 12, 31	wral 2912	. . . . 5 $/\$
33	32, 10, 31	wral 2912	. . . 4 $/\$
34	9, 33	wa 384	. . 3 $/\$ $/\$
35		cmap 7857	. . . 4
36	2, 31, 35	co 6650	. . 3
37	34, 3, 36	crab 2916	. 2 $/\$ $/\$
38	1, 37	wceq 1483	1 $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: ishst 29073

W3C validator