Definition df-hst 32796

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

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-hst

Step	Hyp	Ref	Expression
1		chst 31547	. 2 class CHStates
2		chba 31503	. . . . . . 7 class ℋ
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1569	. . . . . . 7 class 𝑓
5	2, 4	cfv 6531	. . . . . 6 class (𝑓‘ ℋ)
6		cno 31507	. . . . . 6 class normℎ
7	5, 6	cfv 6531	. . . . 5 class (normℎ‘(𝑓‘ ℋ))
8		c1 11182	. . . . 5 class 1
9	7, 8	wceq 1570	. . . 4 wff (normℎ‘(𝑓‘ ℋ)) = 1
10		vx	. . . . . . . . 9 setvar 𝑥
11	10	cv 1569	. . . . . . . 8 class 𝑥
12		vy	. . . . . . . . . 10 setvar 𝑦
13	12	cv 1569	. . . . . . . . 9 class 𝑦
14		cort 31514	. . . . . . . . 9 class ⊥
15	13, 14	cfv 6531	. . . . . . . 8 class (⊥‘𝑦)
16	11, 15	wss 3899	. . . . . . 7 wff 𝑥 ⊆ (⊥‘𝑦)
17	11, 4	cfv 6531	. . . . . . . . . 10 class (𝑓‘𝑥)
18	13, 4	cfv 6531	. . . . . . . . . 10 class (𝑓‘𝑦)
19		csp 31506	. . . . . . . . . 10 class ·ih
20	17, 18, 19	co 7412	. . . . . . . . 9 class ((𝑓‘𝑥) ·ih (𝑓‘𝑦))
21		cc0 11181	. . . . . . . . 9 class 0
22	20, 21	wceq 1570	. . . . . . . 8 wff ((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0
23		chj 31517	. . . . . . . . . . 11 class ∨ℋ
24	11, 13, 23	co 7412	. . . . . . . . . 10 class (𝑥 ∨ℋ 𝑦)
25	24, 4	cfv 6531	. . . . . . . . 9 class (𝑓‘(𝑥 ∨ℋ 𝑦))
26		cva 31504	. . . . . . . . . 10 class +ℎ
27	17, 18, 26	co 7412	. . . . . . . . 9 class ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))
28	25, 27	wceq 1570	. . . . . . . 8 wff (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))
29	22, 28	wa 401	. . . . . . 7 wff (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))
30	16, 29	wi 4	. . . . . 6 wff (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
31		cch 31513	. . . . . 6 class Cℋ
32	30, 12, 31	wral 3077	. . . . 5 wff ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
33	32, 10, 31	wral 3077	. . . 4 wff ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
34	9, 33	wa 401	. . 3 wff ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))
35		cmap 8831	. . . 4 class ↑m
36	2, 31, 35	co 7412	. . 3 class ( ℋ ↑m Cℋ )
37	34, 3, 36	crab 3413	. 2 class {𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}
38	1, 37	wceq 1570	1 wff CHStates = {𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}

This definition is used by:  ishst  32798