Theorem hvaddcani

Description: Cancellation law for vector 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	hvaddcani	$$⊢A{+}_{ℎ}B=A{+}_{ℎ}C\leftrightarrow B=C$$

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		oveq1	$$⊢A{+}_{ℎ}B=A{+}_{ℎ}C\to \left(A{+}_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=\left(A{+}_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
5		neg1cn	$$⊢-1\in ℂ$$
6	5 1	hvmulcli	$$⊢-1{\cdot }_{ℎ}A\in \mathscr{H}$$
7	1 2 6	hvadd32i	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)\right){+}_{ℎ}B$$
8	1	hvnegidi	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=0_{ℎ}$$
9	8	oveq1i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)\right){+}_{ℎ}B=0_{ℎ}{+}_{ℎ}B$$
10	2	hvaddlidi	$$⊢0_{ℎ}{+}_{ℎ}B=B$$
11	7 9 10	3eqtri	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=B$$
12	1 3 6	hvadd32i	$$⊢\left(A{+}_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)\right){+}_{ℎ}C$$
13	8	oveq1i	$$⊢\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)\right){+}_{ℎ}C=0_{ℎ}{+}_{ℎ}C$$
14	3	hvaddlidi	$$⊢0_{ℎ}{+}_{ℎ}C=C$$
15	12 13 14	3eqtri	$$⊢\left(A{+}_{ℎ}C\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=C$$
16	4 11 15	3eqtr3g	$$⊢A{+}_{ℎ}B=A{+}_{ℎ}C\to B=C$$
17		oveq2	$$⊢B=C\to A{+}_{ℎ}B=A{+}_{ℎ}C$$
18	16 17	impbii	$$⊢A{+}_{ℎ}B=A{+}_{ℎ}C\leftrightarrow B=C$$