Theorem hvsubcan2i

Description: Vector cancellation law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	$$⊢A\in \mathscr{H}$$
	hvnegdi.2	$$⊢B\in \mathscr{H}$$
Assertion	hvsubcan2i	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(A{-}_{ℎ}B\right)=2{\cdot }_{ℎ}A$$

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	$$⊢A\in \mathscr{H}$$
2		hvnegdi.2	$$⊢B\in \mathscr{H}$$
3	1 2	hvsubvali	$$⊢A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
4	3	oveq2i	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(A{-}_{ℎ}B\right)=\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
5		neg1cn	$$⊢-1\in ℂ$$
6	5 2	hvmulcli	$$⊢-1{\cdot }_{ℎ}B\in \mathscr{H}$$
7	1 2 1 6	hvadd4i	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=\left(A{+}_{ℎ}A\right){+}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
8		hv2times	$$⊢A\in \mathscr{H}\to 2{\cdot }_{ℎ}A=A{+}_{ℎ}A$$
9	1 8	ax-mp	$$⊢2{\cdot }_{ℎ}A=A{+}_{ℎ}A$$
10	9	eqcomi	$$⊢A{+}_{ℎ}A=2{\cdot }_{ℎ}A$$
11	2	hvnegidi	$$⊢B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=0_{ℎ}$$
12	10 11	oveq12i	$$⊢\left(A{+}_{ℎ}A\right){+}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=\left(2{\cdot }_{ℎ}A\right){+}_{ℎ}{0}_{ℎ}$$
13	7 12	eqtri	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=\left(2{\cdot }_{ℎ}A\right){+}_{ℎ}{0}_{ℎ}$$
14		2cn	$$⊢2\in ℂ$$
15	14 1	hvmulcli	$$⊢2{\cdot }_{ℎ}A\in \mathscr{H}$$
16		ax-hvaddid	$$⊢2{\cdot }_{ℎ}A\in \mathscr{H}\to \left(2{\cdot }_{ℎ}A\right){+}_{ℎ}{0}_{ℎ}=2{\cdot }_{ℎ}A$$
17	15 16	ax-mp	$$⊢\left(2{\cdot }_{ℎ}A\right){+}_{ℎ}{0}_{ℎ}=2{\cdot }_{ℎ}A$$
18	13 17	eqtri	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=2{\cdot }_{ℎ}A$$
19	4 18	eqtri	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(A{-}_{ℎ}B\right)=2{\cdot }_{ℎ}A$$