Definition df-st 30146

Description: Define the set of states on a Hilbert lattice. Definition of [Kalmbach] p. 266. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
df-st	⊢ States = {𝑓 ∈ ((0[,]1) ↑m Cℋ ) ∣ ((𝑓‘ ℋ) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))))}

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-st

Step	Hyp	Ref	Expression
1		cst 28897	. 2 class States
2		chba 28854	. . . . . 6 class ℋ
3		vf	. . . . . . 7 setvar 𝑓
4	3	cv 1541	. . . . . 6 class 𝑓
5	2, 4	cfv 6339	. . . . 5 class (𝑓‘ ℋ)
6		c1 10616	. . . . 5 class 1
7	5, 6	wceq 1542	. . . 4 wff (𝑓‘ ℋ) = 1
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1541	. . . . . . . 8 class 𝑥
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1541	. . . . . . . . 9 class 𝑦
12		cort 28865	. . . . . . . . 9 class ⊥
13	11, 12	cfv 6339	. . . . . . . 8 class (⊥‘𝑦)
14	9, 13	wss 3843	. . . . . . 7 wff 𝑥 ⊆ (⊥‘𝑦)
15		chj 28868	. . . . . . . . . 10 class ∨ℋ
16	9, 11, 15	co 7170	. . . . . . . . 9 class (𝑥 ∨ℋ 𝑦)
17	16, 4	cfv 6339	. . . . . . . 8 class (𝑓‘(𝑥 ∨ℋ 𝑦))
18	9, 4	cfv 6339	. . . . . . . . 9 class (𝑓‘𝑥)
19	11, 4	cfv 6339	. . . . . . . . 9 class (𝑓‘𝑦)
20		caddc 10618	. . . . . . . . 9 class +
21	18, 19, 20	co 7170	. . . . . . . 8 class ((𝑓‘𝑥) + (𝑓‘𝑦))
22	17, 21	wceq 1542	. . . . . . 7 wff (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))
23	14, 22	wi 4	. . . . . 6 wff (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦)))
24		cch 28864	. . . . . 6 class Cℋ
25	23, 10, 24	wral 3053	. . . . 5 wff ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦)))
26	25, 8, 24	wral 3053	. . . 4 wff ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦)))
27	7, 26	wa 399	. . 3 wff ((𝑓‘ ℋ) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))))
28		cc0 10615	. . . . 5 class 0
29		cicc 12824	. . . . 5 class [,]
30	28, 6, 29	co 7170	. . . 4 class (0[,]1)
31		cmap 8437	. . . 4 class ↑m
32	30, 24, 31	co 7170	. . 3 class ((0[,]1) ↑m Cℋ )
33	27, 3, 32	crab 3057	. 2 class {𝑓 ∈ ((0[,]1) ↑m Cℋ ) ∣ ((𝑓‘ ℋ) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))))}
34	1, 33	wceq 1542	1 wff States = {𝑓 ∈ ((0[,]1) ↑m Cℋ ) ∣ ((𝑓‘ ℋ) = 1 ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))))}

This definition is referenced by:  isst  30148