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

Metamath Proof Explorer

Theorem hvsubid

Description: Subtraction of a vector from itself. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsubid ⊢ A ∈ ℋ → A - ℎ A = 0 ℎ

Proof

Step Hyp Ref Expression
1 ax-hvmulid ⊢ A ∈ ℋ → 1 ⋅ ℎ A = A
2 1 oveq1d ⊢ A ∈ ℋ → 1 ⋅ ℎ A + ℎ -1 ⋅ ℎ A = A + ℎ -1 ⋅ ℎ A
3 ax-1cn ⊢ 1 ∈ ℂ
4 neg1cn ⊢ − 1 ∈ ℂ
5 ax-hvdistr2 ⊢ 1 ∈ ℂ ∧ − 1 ∈ ℂ ∧ A ∈ ℋ → 1 + -1 ⋅ ℎ A = 1 ⋅ ℎ A + ℎ -1 ⋅ ℎ A
6 3 4 5 mp3an12 ⊢ A ∈ ℋ → 1 + -1 ⋅ ℎ A = 1 ⋅ ℎ A + ℎ -1 ⋅ ℎ A
7 hvsubval ⊢ A ∈ ℋ ∧ A ∈ ℋ → A - ℎ A = A + ℎ -1 ⋅ ℎ A
8 7 anidms ⊢ A ∈ ℋ → A - ℎ A = A + ℎ -1 ⋅ ℎ A
9 2 6 8 3eqtr4rd ⊢ A ∈ ℋ → A - ℎ A = 1 + -1 ⋅ ℎ A
10 1pneg1e0 ⊢ 1 + -1 = 0
11 10 oveq1i ⊢ 1 + -1 ⋅ ℎ A = 0 ⋅ ℎ A
12 9 11 eqtrdi ⊢ A ∈ ℋ → A - ℎ A = 0 ⋅ ℎ A
13 ax-hvmul0 ⊢ A ∈ ℋ → 0 ⋅ ℎ A = 0 ℎ
14 12 13 eqtrd ⊢ A ∈ ℋ → A - ℎ A = 0 ℎ