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

Metamath Proof Explorer

Theorem pjdsi

Description: Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjsumt.1 
|- G e. CH
pjsumt.2 
|- H e. CH
Assertion pjdsi 
|- ( ( A e. ( G vH H ) /\ G C_ ( _|_ ` H ) ) -> A = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 pjsumt.1 
 |-  G e. CH
2 pjsumt.2 
 |-  H e. CH
3 1 2 osumi 
 |-  ( G C_ ( _|_ ` H ) -> ( G +H H ) = ( G vH H ) )
4 3 fveq2d 
 |-  ( G C_ ( _|_ ` H ) -> ( projh ` ( G +H H ) ) = ( projh ` ( G vH H ) ) )
5 4 fveq1d 
 |-  ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G +H H ) ) ` A ) = ( ( projh ` ( G vH H ) ) ` A ) )
6 1 2 chjcli 
 |-  ( G vH H ) e. CH
7 pjid 
 |-  ( ( ( G vH H ) e. CH /\ A e. ( G vH H ) ) -> ( ( projh ` ( G vH H ) ) ` A ) = A )
8 6 7 mpan 
 |-  ( A e. ( G vH H ) -> ( ( projh ` ( G vH H ) ) ` A ) = A )
9 5 8 sylan9eqr 
 |-  ( ( A e. ( G vH H ) /\ G C_ ( _|_ ` H ) ) -> ( ( projh ` ( G +H H ) ) ` A ) = A )
10 6 cheli 
 |-  ( A e. ( G vH H ) -> A e. ~H )
11 1 2 pjsumi 
 |-  ( A e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G +H H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) ) )
12 11 imp 
 |-  ( ( A e. ~H /\ G C_ ( _|_ ` H ) ) -> ( ( projh ` ( G +H H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) )
13 10 12 sylan 
 |-  ( ( A e. ( G vH H ) /\ G C_ ( _|_ ` H ) ) -> ( ( projh ` ( G +H H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) )
14 9 13 eqtr3d 
 |-  ( ( A e. ( G vH H ) /\ G C_ ( _|_ ` H ) ) -> A = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) )