This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℋ → A + ℎ -1 ⋅ ℎ A = 0 ℎ

Proof

Step Hyp Ref Expression
1 hvsubval ⊢ A ∈ ℋ ∧ A ∈ ℋ → A - ℎ A = A + ℎ -1 ⋅ ℎ A
2 1 anidms ⊢ A ∈ ℋ → A - ℎ A = A + ℎ -1 ⋅ ℎ A
3 hvsubid ⊢ A ∈ ℋ → A - ℎ A = 0 ℎ
4 2 3 eqtr3d ⊢ A ∈ ℋ → A + ℎ -1 ⋅ ℎ A = 0 ℎ