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 ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 𝐴 ) = 0ℎ )

Proof

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