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 ) ) ) )