Metamath Proof Explorer

Theorem pjpjhth

Description: Projection Theorem: Any Hilbert space vector A can be decomposed 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, 6-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjpjhth 
|- ( ( H e. CH /\ A e. ~H ) -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )

Proof

Step Hyp Ref Expression
1 axpjcl 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. H )
2 choccl 
 |-  ( H e. CH -> ( _|_ ` H ) e. CH )
3 axpjcl 
 |-  ( ( ( _|_ ` H ) e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) )
4 2 3 sylan 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) )
5 axpjpj 
 |-  ( ( H e. CH /\ A e. ~H ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
6 rspceov 
 |-  ( ( ( ( projh ` H ) ` A ) e. H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) /\ A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )
7 1 4 5 6 syl3anc 
 |-  ( ( H e. CH /\ A e. ~H ) -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )