pjsubii

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

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

Metamath Proof Explorer