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 + C B = C

Proof

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