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	⊢ CHStates = {𝑓 ∈ ( ℋ ↑𝑚 Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-hst

Step	Hyp	Ref	Expression
1		chst 27820	. 2 class CHStates
2		chil 27776	. . . . . . 7 class ℋ
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1482	. . . . . . 7 class 𝑓
5	2, 4	cfv 5888	. . . . . 6 class (𝑓‘ ℋ)
6		cno 27780	. . . . . 6 class normℎ
7	5, 6	cfv 5888	. . . . 5 class (normℎ‘(𝑓‘ ℋ))
8		c1 9937	. . . . 5 class 1
9	7, 8	wceq 1483	. . . 4 wff (normℎ‘(𝑓‘ ℋ)) = 1
10		vx	. . . . . . . . 9 setvar 𝑥
11	10	cv 1482	. . . . . . . 8 class 𝑥
12		vy	. . . . . . . . . 10 setvar 𝑦
13	12	cv 1482	. . . . . . . . 9 class 𝑦
14		cort 27787	. . . . . . . . 9 class ⊥
15	13, 14	cfv 5888	. . . . . . . 8 class (⊥‘𝑦)
16	11, 15	wss 3574	. . . . . . 7 wff 𝑥 ⊆ (⊥‘𝑦)
17	11, 4	cfv 5888	. . . . . . . . . 10 class (𝑓‘𝑥)
18	13, 4	cfv 5888	. . . . . . . . . 10 class (𝑓‘𝑦)
19		csp 27779	. . . . . . . . . 10 class ·ih
20	17, 18, 19	co 6650	. . . . . . . . 9 class ((𝑓‘𝑥) ·ih (𝑓‘𝑦))
21		cc0 9936	. . . . . . . . 9 class 0
22	20, 21	wceq 1483	. . . . . . . 8 wff ((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0
23		chj 27790	. . . . . . . . . . 11 class ∨ℋ
24	11, 13, 23	co 6650	. . . . . . . . . 10 class (𝑥 ∨ℋ 𝑦)
25	24, 4	cfv 5888	. . . . . . . . 9 class (𝑓‘(𝑥 ∨ℋ 𝑦))
26		cva 27777	. . . . . . . . . 10 class +ℎ
27	17, 18, 26	co 6650	. . . . . . . . 9 class ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))
28	25, 27	wceq 1483	. . . . . . . 8 wff (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))
29	22, 28	wa 384	. . . . . . 7 wff (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))
30	16, 29	wi 4	. . . . . 6 wff (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
31		cch 27786	. . . . . 6 class Cℋ
32	30, 12, 31	wral 2912	. . . . 5 wff ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
33	32, 10, 31	wral 2912	. . . 4 wff ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
34	9, 33	wa 384	. . 3 wff ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))
35		cmap 7857	. . . 4 class ↑𝑚
36	2, 31, 35	co 6650	. . 3 class ( ℋ ↑𝑚 Cℋ )
37	34, 3, 36	crab 2916	. 2 class {𝑓 ∈ ( ℋ ↑𝑚 Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}
38	1, 37	wceq 1483	1 wff CHStates = {𝑓 ∈ ( ℋ ↑𝑚 Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}

This definition is referenced by:  ishst  29073