Metamath Proof Explorer


Theorem hvaddcani

Description: Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvnegdi.1 A
hvnegdi.2 B
hvaddcan.3 C
Assertion hvaddcani A+B=A+CB=C

Proof

Step Hyp Ref Expression
1 hvnegdi.1 A
2 hvnegdi.2 B
3 hvaddcan.3 C
4 oveq1 A+B=A+CA+B+-1A=A+C+-1A
5 neg1cn 1
6 5 1 hvmulcli -1A
7 1 2 6 hvadd32i A+B+-1A=A+-1A+B
8 1 hvnegidi A+-1A=0
9 8 oveq1i A+-1A+B=0+B
10 2 hvaddlidi 0+B=B
11 7 9 10 3eqtri A+B+-1A=B
12 1 3 6 hvadd32i A+C+-1A=A+-1A+C
13 8 oveq1i A+-1A+C=0+C
14 3 hvaddlidi 0+C=C
15 12 13 14 3eqtri A+C+-1A=C
16 4 11 15 3eqtr3g A+B=A+CB=C
17 oveq2 B=CA+B=A+C
18 16 17 impbii A+B=A+CB=C