Theorem pjsubi

Description: Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjadjt.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjsubi	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\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		pjadjt.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		fvoveq1	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A{-}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)$$
3		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
4	3	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
5	2 4	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({\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)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
6		oveq2	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B=if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)$$
7	6	fveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
8		fveq2	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
9	8	oveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
10	7 9	eqeq12d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)\right)$$
11		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
12		ifhvhv0	$$⊢if\left(B\in \mathscr{H},B,0_{ℎ}\right)\in \mathscr{H}$$
13	1 11 12	pjsubii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right){-}_{ℎ}if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
14	5 10 13	dedth2h	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\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)$$