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

Metamath Proof Explorer

Theorem pjhtheu

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. See pjhtheu2 for the uniqueness of y . (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjhth 
 |-  ( H e. CH -> ( H +H ( _|_ ` H ) ) = ~H )
2 1 eleq2d 
 |-  ( H e. CH -> ( A e. ( H +H ( _|_ ` H ) ) <-> A e. ~H ) )
3 chsh 
 |-  ( H e. CH -> H e. SH )
4 shocsh 
 |-  ( H e. SH -> ( _|_ ` H ) e. SH )
5 shsel 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH ) -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
6 3 4 5 syl2anc2 
 |-  ( H e. CH -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
7 2 6 bitr3d 
 |-  ( H e. CH -> ( A e. ~H <-> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
8 7 biimpa 
 |-  ( ( H e. CH /\ A e. ~H ) -> E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )
9 3 4 syl 
 |-  ( H e. CH -> ( _|_ ` H ) e. SH )
10 ocin 
 |-  ( H e. SH -> ( H i^i ( _|_ ` H ) ) = 0H )
11 3 10 syl 
 |-  ( H e. CH -> ( H i^i ( _|_ ` H ) ) = 0H )
12 pjhthmo 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH /\ ( H i^i ( _|_ ` H ) ) = 0H ) -> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
13 3 9 11 12 syl3anc 
 |-  ( H e. CH -> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
14 13 adantr 
 |-  ( ( H e. CH /\ A e. ~H ) -> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
15 reu5 
 |-  ( E! x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) <-> ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
16 df-rmo 
 |-  ( E* x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) <-> E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) )
17 16 anbi2i 
 |-  ( ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) ) <-> ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) ) )
18 15 17 bitri 
 |-  ( E! x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) <-> ( E. x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) /\ E* x ( x e. H /\ E. y e. ( _|_ ` H ) A = ( x +h y ) ) ) )
19 8 14 18 sylanbrc 
 |-  ( ( H e. CH /\ A e. ~H ) -> E! x e. H E. y e. ( _|_ ` H ) A = ( x +h y ) )