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

Definition df-hst 28237
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 = {𝑓 ∈ ( ℋ ↑𝑚 C ) ∣ ((norm‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))))}
Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-hst
StepHypRef Expression
1 chst 26986 . 2 class CHStates
2 chil 26942 . . . . . . 7 class
3 vf . . . . . . . 8 setvar 𝑓
43cv 1473 . . . . . . 7 class 𝑓
52, 4cfv 5694 . . . . . 6 class (𝑓‘ ℋ)
6 cno 26946 . . . . . 6 class norm
75, 6cfv 5694 . . . . 5 class (norm‘(𝑓‘ ℋ))
8 c1 9696 . . . . 5 class 1
97, 8wceq 1474 . . . 4 wff (norm‘(𝑓‘ ℋ)) = 1
10 vx . . . . . . . . 9 setvar 𝑥
1110cv 1473 . . . . . . . 8 class 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1473 . . . . . . . . 9 class 𝑦
14 cort 26953 . . . . . . . . 9 class
1513, 14cfv 5694 . . . . . . . 8 class (⊥‘𝑦)
1611, 15wss 3444 . . . . . . 7 wff 𝑥 ⊆ (⊥‘𝑦)
1711, 4cfv 5694 . . . . . . . . . 10 class (𝑓𝑥)
1813, 4cfv 5694 . . . . . . . . . 10 class (𝑓𝑦)
19 csp 26945 . . . . . . . . . 10 class ·ih
2017, 18, 19co 6431 . . . . . . . . 9 class ((𝑓𝑥) ·ih (𝑓𝑦))
21 cc0 9695 . . . . . . . . 9 class 0
2220, 21wceq 1474 . . . . . . . 8 wff ((𝑓𝑥) ·ih (𝑓𝑦)) = 0
23 chj 26956 . . . . . . . . . . 11 class
2411, 13, 23co 6431 . . . . . . . . . 10 class (𝑥 𝑦)
2524, 4cfv 5694 . . . . . . . . 9 class (𝑓‘(𝑥 𝑦))
26 cva 26943 . . . . . . . . . 10 class +
2717, 18, 26co 6431 . . . . . . . . 9 class ((𝑓𝑥) + (𝑓𝑦))
2825, 27wceq 1474 . . . . . . . 8 wff (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))
2922, 28wa 382 . . . . . . 7 wff (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))
3016, 29wi 4 . . . . . 6 wff (𝑥 ⊆ (⊥‘𝑦) → (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))))
31 cch 26952 . . . . . 6 class C
3230, 12, 31wral 2800 . . . . 5 wff 𝑦C (𝑥 ⊆ (⊥‘𝑦) → (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))))
3332, 10, 31wral 2800 . . . 4 wff 𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦))))
349, 33wa 382 . . 3 wff ((norm‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))))
35 cmap 7624 . . . 4 class 𝑚
362, 31, 35co 6431 . . 3 class ( ℋ ↑𝑚 C )
3734, 3, 36crab 2804 . 2 class {𝑓 ∈ ( ℋ ↑𝑚 C ) ∣ ((norm‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))))}
381, 37wceq 1474 1 wff CHStates = {𝑓 ∈ ( ℋ ↑𝑚 C ) ∣ ((norm‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥C𝑦C (𝑥 ⊆ (⊥‘𝑦) → (((𝑓𝑥) ·ih (𝑓𝑦)) = 0 ∧ (𝑓‘(𝑥 𝑦)) = ((𝑓𝑥) + (𝑓𝑦)))))}
Colors of variables: wff setvar class
This definition is referenced by:  ishst  28239
  Copyright terms: Public domain W3C validator