Theorem pjsubii

Description: Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjidm.1	|- H e. CH
	pjidm.2	|- A e. ~H
	pjsub.3	|- B e. ~H
Assertion	pjsubii	|- ( ( projh ` H ) ` ( A -h B ) ) = ( ( ( projh ` H ) ` A ) -h ( ( projh ` H ) ` B ) )

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	|- H e. CH
2		pjidm.2	|- A e. ~H
3		pjsub.3	|- B e. ~H
4		neg1cn	|- -u 1 e. CC
5	4 3	hvmulcli	|- ( -u 1 .h B ) e. ~H
6	1 2 5	pjaddii	|- ( ( projh ` H ) ` ( A +h ( -u 1 .h B ) ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` ( -u 1 .h B ) ) )
7	1 3 4	pjmulii	|- ( ( projh ` H ) ` ( -u 1 .h B ) ) = ( -u 1 .h ( ( projh ` H ) ` B ) )
8	7	oveq2i	|- ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` ( -u 1 .h B ) ) ) = ( ( ( projh ` H ) ` A ) +h ( -u 1 .h ( ( projh ` H ) ` B ) ) )
9	6 8	eqtri	|- ( ( projh ` H ) ` ( A +h ( -u 1 .h B ) ) ) = ( ( ( projh ` H ) ` A ) +h ( -u 1 .h ( ( projh ` H ) ` B ) ) )
10	2 3	hvsubvali	|- ( A -h B ) = ( A +h ( -u 1 .h B ) )
11	10	fveq2i	|- ( ( projh ` H ) ` ( A -h B ) ) = ( ( projh ` H ) ` ( A +h ( -u 1 .h B ) ) )
12	1 2	pjhclii	|- ( ( projh ` H ) ` A ) e. ~H
13	1 3	pjhclii	|- ( ( projh ` H ) ` B ) e. ~H
14	12 13	hvsubvali	|- ( ( ( projh ` H ) ` A ) -h ( ( projh ` H ) ` B ) ) = ( ( ( projh ` H ) ` A ) +h ( -u 1 .h ( ( projh ` H ) ` B ) ) )
15	9 11 14	3eqtr4i	|- ( ( projh ` H ) ` ( A -h B ) ) = ( ( ( projh ` H ) ` A ) -h ( ( projh ` H ) ` B ) )