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

Definition df-pjh 21804
 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 21347 . 2
2 vh . . 3
3 cch 21339 . . 3
4 vx . . . 4
5 chil 21329 . . . 4
64cv 1618 . . . . . . 7
7 vz . . . . . . . . 9
87cv 1618 . . . . . . . 8
9 vy . . . . . . . . 9
109cv 1618 . . . . . . . 8
11 cva 21330 . . . . . . . 8
128, 10, 11co 5710 . . . . . . 7
136, 12wceq 1619 . . . . . 6
142cv 1618 . . . . . . 7
15 cort 21340 . . . . . . 7
1614, 15cfv 4592 . . . . . 6
1713, 9, 16wrex 2510 . . . . 5
1817, 7, 14crio 6181 . . . 4
194, 5, 18cmpt 3974 . . 3
202, 3, 19cmpt 3974 . 2
211, 20wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  pjhfval  21805  pjmfn  22142
 Copyright terms: Public domain W3C validator