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	⊢ 𝐻 ∈ Cℋ
	pjidm.2	⊢ 𝐴 ∈ ℋ
	pjsub.3	⊢ 𝐵 ∈ ℋ
Assertion	pjsubii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	⊢ 𝐻 ∈ Cℋ
2		pjidm.2	⊢ 𝐴 ∈ ℋ
3		pjsub.3	⊢ 𝐵 ∈ ℋ
4		neg1cn	⊢ - 1 ∈ ℂ
5	4 3	hvmulcli	⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
6	1 2 5	pjaddii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( - 1 ·ℎ 𝐵 ) ) )
7	1 3 4	pjmulii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( - 1 ·ℎ 𝐵 ) ) = ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )
8	7	oveq2i	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
9	6 8	eqtri	⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
10	2 3	hvsubvali	⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
11	10	fveq2i	⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
12	1 2	pjhclii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
13	1 3	pjhclii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ ℋ
14	12 13	hvsubvali	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
15	9 11 14	3eqtr4i	⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )