Theorem hvsubaddi

Description: Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	$$⊢A\in \mathscr{H}$$
	hvnegdi.2	$$⊢B\in \mathscr{H}$$
	hvaddcan.3	$$⊢C\in \mathscr{H}$$
Assertion	hvsubaddi	$$⊢A{-}_{ℎ}B=C\leftrightarrow B{+}_{ℎ}C=A$$

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	$$⊢A\in \mathscr{H}$$
2		hvnegdi.2	$$⊢B\in \mathscr{H}$$
3		hvaddcan.3	$$⊢C\in \mathscr{H}$$
4	1 2	hvsubvali	$$⊢A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
5	4	eqeq1i	$$⊢A{-}_{ℎ}B=C\leftrightarrow A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=C$$
6		neg1cn	$$⊢-1\in ℂ$$
7	6 2	hvmulcli	$$⊢-1{\cdot }_{ℎ}B\in \mathscr{H}$$
8	2 1 7	hvadd12i	$$⊢B{+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=A{+}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
9	2	hvnegidi	$$⊢B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=0_{ℎ}$$
10	9	oveq2i	$$⊢A{+}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=A{+}_{ℎ}{0}_{ℎ}$$
11		ax-hvaddid	$$⊢A\in \mathscr{H}\to A{+}_{ℎ}{0}_{ℎ}=A$$
12	1 11	ax-mp	$$⊢A{+}_{ℎ}{0}_{ℎ}=A$$
13	8 10 12	3eqtri	$$⊢B{+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=A$$
14	13	eqeq1i	$$⊢B{+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=B{+}_{ℎ}C\leftrightarrow A=B{+}_{ℎ}C$$
15	1 7	hvaddcli	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
16	2 15 3	hvaddcani	$$⊢B{+}_{ℎ}\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=B{+}_{ℎ}C\leftrightarrow A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=C$$
17		eqcom	$$⊢A=B{+}_{ℎ}C\leftrightarrow B{+}_{ℎ}C=A$$
18	14 16 17	3bitr3i	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=C\leftrightarrow B{+}_{ℎ}C=A$$
19	5 18	bitri	$$⊢A{-}_{ℎ}B=C\leftrightarrow B{+}_{ℎ}C=A$$