Metamath Proof Explorer

Theorem hvnegidi

Description: Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypothesis hvaddid2.1 
|- A e. ~H
Assertion hvnegidi 
|- ( A +h ( -u 1 .h A ) ) = 0h

Proof

Step Hyp Ref Expression
1 hvaddid2.1 
 |-  A e. ~H
2 hvnegid 
 |-  ( A e. ~H -> ( A +h ( -u 1 .h A ) ) = 0h )
3 1 2 ax-mp 
 |-  ( A +h ( -u 1 .h A ) ) = 0h