Definition df-hst 10096

Description: Define the set of complex Hilbert-space-valued states on a Hilbert lattice. Definition of CH-states in [Mayet3] p. 9.

Assertion

Ref	Expression
df-hst	⊢ CHStates = {f∣(f: Cℋ –→ ℋ ⋀ (normh ‘(f ‘ ℋ )) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y)))))}

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-hst

Step	Hyp	Ref	Expression
1		chst 8787	. 2 class CHStates
2		cch 8753	. . . . 5 class Cℋ
3		chil 8743	. . . . 5 class ℋ
4		vf	. . . . . 6 set f
5	4	cv 954	. . . . 5 class f
6	2, 3, 5	wf 3174	. . . 4 wff f: Cℋ –→ ℋ
7	3, 5	cfv 3178	. . . . . 6 class (f ‘ ℋ )
8		cno 8749	. . . . . 6 class normh
9	7, 8	cfv 3178	. . . . 5 class (normh ‘(f ‘ ℋ ))
10		c1 5218	. . . . 5 class 1
11	9, 10	wceq 955	. . . 4 wff (normh ‘(f ‘ ℋ )) = 1
12		vx	. . . . . . . . 9 set x
13	12	cv 954	. . . . . . . 8 class x
14		vy	. . . . . . . . . 10 set y
15	14	cv 954	. . . . . . . . 9 class y
16		cort 8754	. . . . . . . . 9 class ⊥
17	15, 16	cfv 3178	. . . . . . . 8 class (⊥ ‘y)
18	13, 17	wss 2044	. . . . . . 7 wff x ⊆ (⊥ ‘y)
19	13, 5	cfv 3178	. . . . . . . . . 10 class (f ‘x)
20	15, 5	cfv 3178	. . . . . . . . . 10 class (f ‘y)
21		csp 8748	. . . . . . . . . 10 class ·ih
22	19, 20, 21	co 3958	. . . . . . . . 9 class ((f ‘x) ·ih (f ‘y))
23		cc0 5217	. . . . . . . . 9 class 0
24	22, 23	wceq 955	. . . . . . . 8 wff ((f ‘x) ·ih (f ‘y)) = 0
25		chj 8757	. . . . . . . . . . 11 class ∨ℋ
26	13, 15, 25	co 3958	. . . . . . . . . 10 class (x ∨ℋ y)
27	26, 5	cfv 3178	. . . . . . . . 9 class (f ‘(x ∨ℋ y))
28		cva 8744	. . . . . . . . . 10 class +h
29	19, 20, 28	co 3958	. . . . . . . . 9 class ((f ‘x) +h (f ‘y))
30	27, 29	wceq 955	. . . . . . . 8 wff (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y))
31	24, 30	wa 223	. . . . . . 7 wff (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y)))
32	18, 31	wi 3	. . . . . 6 wff (x ⊆ (⊥ ‘y) → (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y))))
33	32, 14, 2	wral 1643	. . . . 5 wff ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y))))
34	33, 12, 2	wral 1643	. . . 4 wff ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y))))
35	6, 11, 34	w3a 774	. . 3 wff (f: Cℋ –→ ℋ ⋀ (normh ‘(f ‘ ℋ )) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y)))))
36	35, 4	cab 1462	. 2 class {f∣(f: Cℋ –→ ℋ ⋀ (normh ‘(f ‘ ℋ )) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y)))))}
37	1, 36	wceq 955	1 wff CHStates = {f∣(f: Cℋ –→ ℋ ⋀ (normh ‘(f ‘ ℋ )) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (((f ‘x) ·ih (f ‘y)) = 0 ⋀ (f ‘(x ∨ℋ y)) = ((f ‘x) +h (f ‘y)))))}

This definition is referenced by:  hstelt 10098

Copyright terms: Public domain