Definition df-hst 30475

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 29226	. 2 class CHStates
2		chba 29182	. . . . . . 7 class ℋ
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1538	. . . . . . 7 class 𝑓
5	2, 4	cfv 6418	. . . . . 6 class (𝑓‘ ℋ)
6		cno 29186	. . . . . 6 class normℎ
7	5, 6	cfv 6418	. . . . 5 class (normℎ‘(𝑓‘ ℋ))
8		c1 10803	. . . . 5 class 1
9	7, 8	wceq 1539	. . . 4 wff (normℎ‘(𝑓‘ ℋ)) = 1
10		vx	. . . . . . . . 9 setvar 𝑥
11	10	cv 1538	. . . . . . . 8 class 𝑥
12		vy	. . . . . . . . . 10 setvar 𝑦
13	12	cv 1538	. . . . . . . . 9 class 𝑦
14		cort 29193	. . . . . . . . 9 class ⊥
15	13, 14	cfv 6418	. . . . . . . 8 class (⊥‘𝑦)
16	11, 15	wss 3883	. . . . . . 7 wff 𝑥 ⊆ (⊥‘𝑦)
17	11, 4	cfv 6418	. . . . . . . . . 10 class (𝑓‘𝑥)
18	13, 4	cfv 6418	. . . . . . . . . 10 class (𝑓‘𝑦)
19		csp 29185	. . . . . . . . . 10 class ·ih
20	17, 18, 19	co 7255	. . . . . . . . 9 class ((𝑓‘𝑥) ·ih (𝑓‘𝑦))
21		cc0 10802	. . . . . . . . 9 class 0
22	20, 21	wceq 1539	. . . . . . . 8 wff ((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0
23		chj 29196	. . . . . . . . . . 11 class ∨ℋ
24	11, 13, 23	co 7255	. . . . . . . . . 10 class (𝑥 ∨ℋ 𝑦)
25	24, 4	cfv 6418	. . . . . . . . 9 class (𝑓‘(𝑥 ∨ℋ 𝑦))
26		cva 29183	. . . . . . . . . 10 class +ℎ
27	17, 18, 26	co 7255	. . . . . . . . 9 class ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))
28	25, 27	wceq 1539	. . . . . . . 8 wff (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))
29	22, 28	wa 395	. . . . . . 7 wff (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))
30	16, 29	wi 4	. . . . . 6 wff (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
31		cch 29192	. . . . . 6 class Cℋ
32	30, 12, 31	wral 3063	. . . . 5 wff ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
33	32, 10, 31	wral 3063	. . . 4 wff ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))
34	9, 33	wa 395	. . 3 wff ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))
35		cmap 8573	. . . 4 class ↑m
36	2, 31, 35	co 7255	. . 3 class ( ℋ ↑m Cℋ )
37	34, 3, 36	crab 3067	. 2 class {𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}
38	1, 37	wceq 1539	1 wff CHStates = {𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))}

This definition is referenced by:  ishst  30477