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

Definition df-pjh 24625
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 h `  H
) `  A is the projection of vector  A onto closed subspace  H. Note that the range of  proj h is the set of all projection operators, so  T  e.  ran  proj h means that  T is a projection operator. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
Assertion
Ref Expression
df-pjh  |-  proj h  =  ( h  e.  CH  |->  ( x  e.  ~H  |->  ( iota_ z  e.  h  E. y  e.  ( _|_ `  h ) x  =  ( z  +h  y ) ) ) )
Distinct variable group:    x, h, y, z

Detailed syntax breakdown of Definition df-pjh
StepHypRef Expression
1 cpjh 24166 . 2  class  proj h
2 vh . . 3  setvar  h
3 cch 24158 . . 3  class  CH
4 vx . . . 4  setvar  x
5 chil 24148 . . . 4  class  ~H
64cv 1363 . . . . . . 7  class  x
7 vz . . . . . . . . 9  setvar  z
87cv 1363 . . . . . . . 8  class  z
9 vy . . . . . . . . 9  setvar  y
109cv 1363 . . . . . . . 8  class  y
11 cva 24149 . . . . . . . 8  class  +h
128, 10, 11co 6084 . . . . . . 7  class  ( z  +h  y )
136, 12wceq 1364 . . . . . 6  wff  x  =  ( z  +h  y
)
142cv 1363 . . . . . . 7  class  h
15 cort 24159 . . . . . . 7  class  _|_
1614, 15cfv 5410 . . . . . 6  class  ( _|_ `  h )
1713, 9, 16wrex 2710 . . . . 5  wff  E. y  e.  ( _|_ `  h
) x  =  ( z  +h  y )
1817, 7, 14crio 6042 . . . 4  class  ( iota_ z  e.  h  E. y  e.  ( _|_ `  h
) x  =  ( z  +h  y ) )
194, 5, 18cmpt 4342 . . 3  class  ( x  e.  ~H  |->  ( iota_ z  e.  h  E. y  e.  ( _|_ `  h
) x  =  ( z  +h  y ) ) )
202, 3, 19cmpt 4342 . 2  class  ( h  e.  CH  |->  ( x  e.  ~H  |->  ( iota_ z  e.  h  E. y  e.  ( _|_ `  h
) x  =  ( z  +h  y ) ) ) )
211, 20wceq 1364 1  wff  proj h  =  ( h  e.  CH  |->  ( x  e.  ~H  |->  ( iota_ z  e.  h  E. y  e.  ( _|_ `  h ) x  =  ( z  +h  y ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  pjhfval  24626  pjmfn  24945
  Copyright terms: Public domain W3C validator