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