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

Definition df-pjh 27426
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 26966 . 2 class proj
2 vh . . 3 setvar
3 cch 26958 . . 3 class C
4 vx . . . 4 setvar 𝑥
5 chil 26948 . . . 4 class
64cv 1473 . . . . . . 7 class 𝑥
7 vz . . . . . . . . 9 setvar 𝑧
87cv 1473 . . . . . . . 8 class 𝑧
9 vy . . . . . . . . 9 setvar 𝑦
109cv 1473 . . . . . . . 8 class 𝑦
11 cva 26949 . . . . . . . 8 class +
128, 10, 11co 6426 . . . . . . 7 class (𝑧 + 𝑦)
136, 12wceq 1474 . . . . . 6 wff 𝑥 = (𝑧 + 𝑦)
142cv 1473 . . . . . . 7 class
15 cort 26959 . . . . . . 7 class
1614, 15cfv 5689 . . . . . 6 class (⊥‘)
1713, 9, 16wrex 2801 . . . . 5 wff 𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦)
1817, 7, 14crio 6387 . . . 4 class (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦))
194, 5, 18cmpt 4541 . . 3 class (𝑥 ∈ ℋ ↦ (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦)))
202, 3, 19cmpt 4541 . 2 class (C ↦ (𝑥 ∈ ℋ ↦ (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦))))
211, 20wceq 1474 1 wff proj = (C ↦ (𝑥 ∈ ℋ ↦ (𝑧𝑦 ∈ (⊥‘)𝑥 = (𝑧 + 𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  pjhfval  27427  pjmfn  27746
  Copyright terms: Public domain W3C validator