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 hvaddlid.1 
|- A e. ~H
Assertion hv2negi 
|- ( 0h -h A ) = ( -u 1 .h A )

Proof

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