Metamath Proof Explorer


Theorem hvsubid

Description: Subtraction of a vector from itself. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsubid A A - A = 0

Proof

Step Hyp Ref Expression
1 ax-hvmulid A 1 A = A
2 1 oveq1d A 1 A + -1 A = A + -1 A
3 ax-1cn 1
4 neg1cn 1
5 ax-hvdistr2 1 1 A 1 + -1 A = 1 A + -1 A
6 3 4 5 mp3an12 A 1 + -1 A = 1 A + -1 A
7 hvsubval A A A - A = A + -1 A
8 7 anidms A A - A = A + -1 A
9 2 6 8 3eqtr4rd A A - A = 1 + -1 A
10 1pneg1e0 1 + -1 = 0
11 10 oveq1i 1 + -1 A = 0 A
12 9 11 eqtrdi A A - A = 0 A
13 ax-hvmul0 A 0 A = 0
14 12 13 eqtrd A A - A = 0