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

Metamath Proof Explorer

Theorem pjsumi

Description: The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjsumt.1 
|- G e. CH
pjsumt.2 
|- H e. CH
Assertion pjsumi 
|- ( A e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G +H 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 5 adantl 
 |-  ( ( A e. ~H /\ G C_ ( _|_ ` H ) ) -> ( ( projh ` ( G +H H ) ) ` A ) = ( ( projh ` ( G vH H ) ) ` A ) )
7 pjcjt2 
 |-  ( ( G e. CH /\ H e. CH /\ A e. ~H ) -> ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G vH H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) ) )
8 1 2 7 mp3an12 
 |-  ( A e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G vH H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) ) )
9 8 imp 
 |-  ( ( A e. ~H /\ G C_ ( _|_ ` H ) ) -> ( ( projh ` ( G vH H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) )
10 6 9 eqtrd 
 |-  ( ( A e. ~H /\ G C_ ( _|_ ` H ) ) -> ( ( projh ` ( G +H H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) )
11 10 ex 
 |-  ( A e. ~H -> ( G C_ ( _|_ ` H ) -> ( ( projh ` ( G +H H ) ) ` A ) = ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) ) )