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\in {\mathbf{C}}_{\mathscr{H}}$$
	pjidm.2	$$⊢A\in \mathscr{H}$$
	pjsub.3	$$⊢B\in \mathscr{H}$$
Assertion	pjsubii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{-}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3		pjsub.3	$$⊢B\in \mathscr{H}$$
4		neg1cn	$$⊢-1\in ℂ$$
5	4 3	hvmulcli	$$⊢-1{\cdot }_{ℎ}B\in \mathscr{H}$$
6	1 2 5	pjaddii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(-1{\cdot }_{ℎ}B\right)$$
7	1 3 4	pjmulii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(-1{\cdot }_{ℎ}B\right)=-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
8	7	oveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(-1{\cdot }_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
9	6 8	eqtri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
10	2 3	hvsubvali	$$⊢A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
11	10	fveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{-}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
12	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
13	1 3	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in \mathscr{H}$$
14	12 13	hvsubvali	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
15	9 11 14	3eqtr4i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A{-}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$