Metamath Proof Explorer

Theorem hvnegid

Description: Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion hvnegid 
|- ( A e. ~H -> ( A +h ( -u 1 .h A ) ) = 0h )

Proof

Step Hyp Ref Expression
1 hvsubval 
 |-  ( ( A e. ~H /\ A e. ~H ) -> ( A -h A ) = ( A +h ( -u 1 .h A ) ) )
2 1 anidms 
 |-  ( A e. ~H -> ( A -h A ) = ( A +h ( -u 1 .h A ) ) )
3 hvsubid 
 |-  ( A e. ~H -> ( A -h A ) = 0h )
4 2 3 eqtr3d 
 |-  ( A e. ~H -> ( A +h ( -u 1 .h A ) ) = 0h )