Theorem pjssumi

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	pjco.1	|- G e. CH
	pjco.2	|- H e. CH
Assertion	pjssumi	|- ( G C_ ( _|_ ` H ) -> ( projh ` ( G +H H ) ) = ( ( projh ` G ) +op ( projh ` H ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjco.1	|- G e. CH
2		pjco.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	1 2	pjscji	|- ( G C_ ( _|_ ` H ) -> ( projh ` ( G vH H ) ) = ( ( projh ` G ) +op ( projh ` H ) ) )
6	4 5	eqtrd	|- ( G C_ ( _|_ ` H ) -> ( projh ` ( G +H H ) ) = ( ( projh ` G ) +op ( projh ` H ) ) )