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

Definition df-pjh 22899
 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. is the projection of vector onto closed subspace . Note that the range of is the set of all projection operators, so means that is a projection operator. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
Assertion
Ref Expression
df-pjh
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-pjh
StepHypRef Expression
1 cpjh 22442 . 2
2 vh . . 3
3 cch 22434 . . 3
4 vx . . . 4
5 chil 22424 . . . 4
64cv 1652 . . . . . . 7
7 vz . . . . . . . . 9
87cv 1652 . . . . . . . 8
9 vy . . . . . . . . 9
109cv 1652 . . . . . . . 8
11 cva 22425 . . . . . . . 8
128, 10, 11co 6083 . . . . . . 7
136, 12wceq 1653 . . . . . 6
142cv 1652 . . . . . . 7
15 cort 22435 . . . . . . 7
1614, 15cfv 5456 . . . . . 6
1713, 9, 16wrex 2708 . . . . 5
1817, 7, 14crio 6544 . . . 4
194, 5, 18cmpt 4268 . . 3
202, 3, 19cmpt 4268 . 2
211, 20wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  pjhfval  22900  pjmfn  23219
 Copyright terms: Public domain W3C validator