Definition df-st 10049

Description: Define the set of states on a Hilbert lattice. Definition of [Kalmbach] p. 266.

Assertion

Ref	Expression
df-st	⊢ States = {f∣((f: Cℋ –→ℝ ⋀ ∀x ∈ Cℋ (0 ≤ (f ‘x) ⋀ (f ‘x) ≤ 1)) ⋀ ((f ‘ ℋ ) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))))}

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-st

Step	Hyp	Ref	Expression
1		cst 8770	. 2 class States
2		cch 8737	. . . . . 6 class Cℋ
3		cr 5205	. . . . . 6 class ℝ
4		vf	. . . . . . 7 set f
5	4	cv 952	. . . . . 6 class f
6	2, 3, 5	wf 3168	. . . . 5 wff f: Cℋ –→ℝ
7		cc0 5206	. . . . . . . 8 class 0
8		vx	. . . . . . . . . 10 set x
9	8	cv 952	. . . . . . . . 9 class x
10	9, 5	cfv 3172	. . . . . . . 8 class (f ‘x)
11		cle 5267	. . . . . . . 8 class ≤
12	7, 10, 11	wbr 2609	. . . . . . 7 wff 0 ≤ (f ‘x)
13		c1 5207	. . . . . . . 8 class 1
14	10, 13, 11	wbr 2609	. . . . . . 7 wff (f ‘x) ≤ 1
15	12, 14	wa 223	. . . . . 6 wff (0 ≤ (f ‘x) ⋀ (f ‘x) ≤ 1)
16	15, 8, 2	wral 1637	. . . . 5 wff ∀x ∈ Cℋ (0 ≤ (f ‘x) ⋀ (f ‘x) ≤ 1)
17	6, 16	wa 223	. . . 4 wff (f: Cℋ –→ℝ ⋀ ∀x ∈ Cℋ (0 ≤ (f ‘x) ⋀ (f ‘x) ≤ 1))
18		chil 8727	. . . . . . 7 class ℋ
19	18, 5	cfv 3172	. . . . . 6 class (f ‘ ℋ )
20	19, 13	wceq 953	. . . . 5 wff (f ‘ ℋ ) = 1
21		vy	. . . . . . . . . . 11 set y
22	21	cv 952	. . . . . . . . . 10 class y
23		cort 8738	. . . . . . . . . 10 class ⊥
24	22, 23	cfv 3172	. . . . . . . . 9 class (⊥ ‘y)
25	9, 24	wss 2037	. . . . . . . 8 wff x ⊆ (⊥ ‘y)
26		chj 8741	. . . . . . . . . . 11 class ∨ℋ
27	9, 22, 26	co 3948	. . . . . . . . . 10 class (x ∨ℋ y)
28	27, 5	cfv 3172	. . . . . . . . 9 class (f ‘(x ∨ℋ y))
29	22, 5	cfv 3172	. . . . . . . . . 10 class (f ‘y)
30		caddc 5209	. . . . . . . . . 10 class +
31	10, 29, 30	co 3948	. . . . . . . . 9 class ((f ‘x) + (f ‘y))
32	28, 31	wceq 953	. . . . . . . 8 wff (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y))
33	25, 32	wi 3	. . . . . . 7 wff (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))
34	33, 21, 2	wral 1637	. . . . . 6 wff ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))
35	34, 8, 2	wral 1637	. . . . 5 wff ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))
36	20, 35	wa 223	. . . 4 wff ((f ‘ ℋ ) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y))))
37	17, 36	wa 223	. . 3 wff ((f: Cℋ –→ℝ ⋀ ∀x ∈ Cℋ (0 ≤ (f ‘x) ⋀ (f ‘x) ≤ 1)) ⋀ ((f ‘ ℋ ) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))))
38	37, 4	cab 1456	. 2 class {f∣((f: Cℋ –→ℝ ⋀ ∀x ∈ Cℋ (0 ≤ (f ‘x) ⋀ (f ‘x) ≤ 1)) ⋀ ((f ‘ ℋ ) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))))}
39	1, 38	wceq 953	1 wff States = {f∣((f: Cℋ –→ℝ ⋀ ∀x ∈ Cℋ (0 ≤ (f ‘x) ⋀ (f ‘x) ≤ 1)) ⋀ ((f ‘ ℋ ) = 1 ⋀ ∀x ∈ Cℋ ∀y ∈ Cℋ (x ⊆ (⊥ ‘y) → (f ‘(x ∨ℋ y)) = ((f ‘x) + (f ‘y)))))}

This definition is referenced by:  stelt 10051

Copyright terms: Public domain