Theorem pjpj0i

Description: Decomposition of a vector into projections. (Contributed by NM, 26-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjcli.1	|- H e. CH
	pjcli.2	|- A e. ~H
Assertion	pjpj0i	|- A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		pjcli.1	|- H e. CH
2		pjcli.2	|- A e. ~H
3		axpjpj	|- ( ( H e. CH /\ A e. ~H ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
4	1 2 3	mp2an	|- A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )