Metamath Proof Explorer


Theorem hv2negi

Description: Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis hvaddid2.1 A
Assertion hv2negi 0 - A = -1 A

Proof

Step Hyp Ref Expression
1 hvaddid2.1 A
2 hv2neg A 0 - A = -1 A
3 1 2 ax-mp 0 - A = -1 A