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

Definition df-pjh 27638
 Description: Define the projection function on a Hilbert space, as a mapping from the Hilbert lattice to a function on Hilbert space. Every closed subspace is associated with a unique projection function. Remark in [Kalmbach] p. 66, adopted as a definition. (projℎ‘𝐻)‘𝐴 is the projection of vector 𝐴 onto closed subspace 𝐻. Note that the range of projℎ is the set of all projection operators, so 𝑇 ∈ ran projℎ means that 𝑇 is a projection operator. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
Assertion
Ref Expression
df-pjh proj = (C ↦ (𝑥 ∈ ℋ ↦ (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦))))
Distinct variable group:   𝑥,,𝑦,𝑧

Detailed syntax breakdown of Definition df-pjh
StepHypRef Expression
1 cpjh 27178 . 2 class proj
2 vh . . 3 setvar
3 cch 27170 . . 3 class C
4 vx . . . 4 setvar 𝑥
5 chil 27160 . . . 4 class
64cv 1474 . . . . . . 7 class 𝑥
7 vz . . . . . . . . 9 setvar 𝑧
87cv 1474 . . . . . . . 8 class 𝑧
9 vy . . . . . . . . 9 setvar 𝑦
109cv 1474 . . . . . . . 8 class 𝑦
11 cva 27161 . . . . . . . 8 class +
128, 10, 11co 6549 . . . . . . 7 class (𝑧 + 𝑦)
136, 12wceq 1475 . . . . . 6 wff 𝑥 = (𝑧 + 𝑦)
142cv 1474 . . . . . . 7 class
15 cort 27171 . . . . . . 7 class
1614, 15cfv 5804 . . . . . 6 class (⊥‘)
1713, 9, 16wrex 2897 . . . . 5 wff 𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦)
1817, 7, 14crio 6510 . . . 4 class (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦))
194, 5, 18cmpt 4643 . . 3 class (𝑥 ∈ ℋ ↦ (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦)))
202, 3, 19cmpt 4643 . 2 class (C ↦ (𝑥 ∈ ℋ ↦ (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦))))
211, 20wceq 1475 1 wff proj = (C ↦ (𝑥 ∈ ℋ ↦ (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦))))
 Colors of variables: wff setvar class This definition is referenced by:  pjhfval  27639  pjmfn  27958
 Copyright terms: Public domain W3C validator