Theorem hvsubeq0i

Description: If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	$$⊢A\in \mathscr{H}$$
	hvnegdi.2	$$⊢B\in \mathscr{H}$$
Assertion	hvsubeq0i	$$⊢A{-}_{ℎ}B=0_{ℎ}\leftrightarrow A=B$$

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	eqeq1i	$$⊢A{-}_{ℎ}B=0_{ℎ}\leftrightarrow A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=0_{ℎ}$$
5		oveq1	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=0_{ℎ}\to \left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}B=0_{ℎ}{+}_{ℎ}B$$
6	4 5	sylbi	$$⊢A{-}_{ℎ}B=0_{ℎ}\to \left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}B=0_{ℎ}{+}_{ℎ}B$$
7		neg1cn	$$⊢-1\in ℂ$$
8	7 2	hvmulcli	$$⊢-1{\cdot }_{ℎ}B\in \mathscr{H}$$
9	1 8 2	hvadd32i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}B=\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
10	1 2 8	hvassi	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=A{+}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
11	2	hvnegidi	$$⊢B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=0_{ℎ}$$
12	11	oveq2i	$$⊢A{+}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=A{+}_{ℎ}{0}_{ℎ}$$
13		ax-hvaddid	$$⊢A\in \mathscr{H}\to A{+}_{ℎ}{0}_{ℎ}=A$$
14	1 13	ax-mp	$$⊢A{+}_{ℎ}{0}_{ℎ}=A$$
15	12 14	eqtri	$$⊢A{+}_{ℎ}\left(B{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=A$$
16	10 15	eqtri	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)=A$$
17	9 16	eqtri	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right){+}_{ℎ}B=A$$
18	2	hvaddlidi	$$⊢0_{ℎ}{+}_{ℎ}B=B$$
19	6 17 18	3eqtr3g	$$⊢A{-}_{ℎ}B=0_{ℎ}\to A=B$$
20		oveq1	$$⊢A=B\to A{-}_{ℎ}B=B{-}_{ℎ}B$$
21		hvsubid	$$⊢B\in \mathscr{H}\to B{-}_{ℎ}B=0_{ℎ}$$
22	2 21	ax-mp	$$⊢B{-}_{ℎ}B=0_{ℎ}$$
23	20 22	eqtrdi	$$⊢A=B\to A{-}_{ℎ}B=0_{ℎ}$$
24	19 23	impbii	$$⊢A{-}_{ℎ}B=0_{ℎ}\leftrightarrow A=B$$