Metamath Proof Explorer


Theorem hvaddsubval

Description: Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hvaddsubval A B A + B = A - -1 B

Proof

Step Hyp Ref Expression
1 neg1cn 1
2 hvmulcl 1 B -1 B
3 1 2 mpan B -1 B
4 hvsubval A -1 B A - -1 B = A + -1 -1 B
5 3 4 sylan2 A B A - -1 B = A + -1 -1 B
6 hvm1neg 1 B -1 -1 B = -1 B
7 1 6 mpan B -1 -1 B = -1 B
8 negneg1e1 -1 = 1
9 8 oveq1i -1 B = 1 B
10 7 9 eqtrdi B -1 -1 B = 1 B
11 ax-hvmulid B 1 B = B
12 10 11 eqtrd B -1 -1 B = B
13 12 adantl A B -1 -1 B = B
14 13 oveq2d A B A + -1 -1 B = A + B
15 5 14 eqtr2d A B A + B = A - -1 B