HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-st Structured version   Visualization version   GIF version

Definition df-st 29410
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) ↑𝑚 C ) ∣ ((𝑓‘ ℋ) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))))}
Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-st
StepHypRef Expression
1 cst 28159 . 2 class States
2 chil 28116 . . . . . 6 class
3 vf . . . . . . 7 setvar 𝑓
43cv 1630 . . . . . 6 class 𝑓
52, 4cfv 6031 . . . . 5 class (𝑓‘ ℋ)
6 c1 10139 . . . . 5 class 1
75, 6wceq 1631 . . . 4 wff (𝑓‘ ℋ) = 1
8 vx . . . . . . . . 9 setvar 𝑥
98cv 1630 . . . . . . . 8 class 𝑥
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1630 . . . . . . . . 9 class 𝑦
12 cort 28127 . . . . . . . . 9 class
1311, 12cfv 6031 . . . . . . . 8 class (⊥‘𝑦)
149, 13wss 3723 . . . . . . 7 wff 𝑥 ⊆ (⊥‘𝑦)
15 chj 28130 . . . . . . . . . 10 class
169, 11, 15co 6793 . . . . . . . . 9 class (𝑥 𝑦)
1716, 4cfv 6031 . . . . . . . 8 class (𝑓‘(𝑥 𝑦))
189, 4cfv 6031 . . . . . . . . 9 class (𝑓𝑥)
1911, 4cfv 6031 . . . . . . . . 9 class (𝑓𝑦)
20 caddc 10141 . . . . . . . . 9 class +
2118, 19, 20co 6793 . . . . . . . 8 class ((𝑓𝑥) + (𝑓𝑦))
2217, 21wceq 1631 . . . . . . 7 wff (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))
2314, 22wi 4 . . . . . 6 wff (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))
24 cch 28126 . . . . . 6 class C
2523, 10, 24wral 3061 . . . . 5 wff 𝑦C (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))
2625, 8, 24wral 3061 . . . 4 wff 𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))
277, 26wa 382 . . 3 wff ((𝑓‘ ℋ) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))))
28 cc0 10138 . . . . 5 class 0
29 cicc 12383 . . . . 5 class [,]
3028, 6, 29co 6793 . . . 4 class (0[,]1)
31 cmap 8009 . . . 4 class 𝑚
3230, 24, 31co 6793 . . 3 class ((0[,]1) ↑𝑚 C )
3327, 3, 32crab 3065 . 2 class {𝑓 ∈ ((0[,]1) ↑𝑚 C ) ∣ ((𝑓‘ ℋ) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))))}
341, 33wceq 1631 1 wff States = {𝑓 ∈ ((0[,]1) ↑𝑚 C ) ∣ ((𝑓‘ ℋ) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  isst  29412
  Copyright terms: Public domain W3C validator