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=-1A

Proof

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