Metamath Proof Explorer

Theorem pjhth

Description: Projection Theorem: Any Hilbert space vector A can be decomposed uniquely into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of Beran p. 102 (existence part). (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhth 
|- ( H e. CH -> ( H +H ( _|_ ` H ) ) = ~H )

Proof

Step Hyp Ref Expression
1 chsh 
 |-  ( H e. CH -> H e. SH )
2 shocsh 
 |-  ( H e. SH -> ( _|_ ` H ) e. SH )
3 shsss 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH ) -> ( H +H ( _|_ ` H ) ) C_ ~H )
4 1 2 3 syl2anc2 
 |-  ( H e. CH -> ( H +H ( _|_ ` H ) ) C_ ~H )
5 fveq2 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( _|_ ` H ) = ( _|_ ` if ( H e. CH , H , ~H ) ) )
6 5 rexeqdv 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( E. z e. ( _|_ ` H ) x = ( y +h z ) <-> E. z e. ( _|_ ` if ( H e. CH , H , ~H ) ) x = ( y +h z ) ) )
7 6 rexeqbi1dv 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( E. y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) <-> E. y e. if ( H e. CH , H , ~H ) E. z e. ( _|_ ` if ( H e. CH , H , ~H ) ) x = ( y +h z ) ) )
8 7 imbi2d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( x e. ~H -> E. y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) ) <-> ( x e. ~H -> E. y e. if ( H e. CH , H , ~H ) E. z e. ( _|_ ` if ( H e. CH , H , ~H ) ) x = ( y +h z ) ) ) )
9 ifchhv 
 |-  if ( H e. CH , H , ~H ) e. CH
10 id 
 |-  ( x e. ~H -> x e. ~H )
11 9 10 pjhthlem2 
 |-  ( x e. ~H -> E. y e. if ( H e. CH , H , ~H ) E. z e. ( _|_ ` if ( H e. CH , H , ~H ) ) x = ( y +h z ) )
12 8 11 dedth 
 |-  ( H e. CH -> ( x e. ~H -> E. y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) ) )
13 shsel 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH ) -> ( x e. ( H +H ( _|_ ` H ) ) <-> E. y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) ) )
14 1 2 13 syl2anc2 
 |-  ( H e. CH -> ( x e. ( H +H ( _|_ ` H ) ) <-> E. y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) ) )
15 12 14 sylibrd 
 |-  ( H e. CH -> ( x e. ~H -> x e. ( H +H ( _|_ ` H ) ) ) )
16 15 ssrdv 
 |-  ( H e. CH -> ~H C_ ( H +H ( _|_ ` H ) ) )
17 4 16 eqssd 
 |-  ( H e. CH -> ( H +H ( _|_ ` H ) ) = ~H )