This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-pjh

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. ( projhH )A is the projection of vector A onto closed subspace H . Note that the range of projh is the set of all projection operators, so T e. ran projh means that T is a projection operator. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion df-pjh 
|- projh = ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpjh 
 |-  projh
1 vh 
 |-  h
2 cch 
 |-  CH
3 vx 
 |-  x
4 chba 
 |-  ~H
5 vz 
 |-  z
6 1 cv 
 |-  h
7 vy 
 |-  y
8 cort 
 |-  _|_
9 6 8 cfv 
 |-  ( _|_ ` h )
10 3 cv 
 |-  x
11 5 cv 
 |-  z
12 cva 
 |-  +h
13 7 cv 
 |-  y
14 11 13 12 co 
 |-  ( z +h y )
15 10 14 wceq 
 |-  x = ( z +h y )
16 15 7 9 wrex 
 |-  E. y e. ( _|_ ` h ) x = ( z +h y )
17 16 5 6 crio 
 |-  ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) )
18 3 4 17 cmpt 
 |-  ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) )
19 1 2 18 cmpt 
 |-  ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )
20 0 19 wceq 
 |-  projh = ( h e. CH |-> ( x e. ~H |-> ( iota_ z e. h E. y e. ( _|_ ` h ) x = ( z +h y ) ) ) )