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

Metamath Proof Explorer

Theorem normneg

Description: The norm of a vector equals the norm of its negative. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

Ref Expression
Assertion normneg ( 𝐴 ∈ ℋ → ( normℎ ‘ ( - 1 ·ℎ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ax-hv0cl ⊢ 0ℎ ∈ ℋ
2 normsub ⊢ ( ( 0ℎ ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 0ℎ −ℎ 𝐴 ) ) = ( normℎ ‘ ( 𝐴 −ℎ 0ℎ ) ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 0ℎ −ℎ 𝐴 ) ) = ( normℎ ‘ ( 𝐴 −ℎ 0ℎ ) ) )
4 hv2neg ⊢ ( 𝐴 ∈ ℋ → ( 0ℎ −ℎ 𝐴 ) = ( - 1 ·ℎ 𝐴 ) )
5 4 fveq2d ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 0ℎ −ℎ 𝐴 ) ) = ( normℎ ‘ ( - 1 ·ℎ 𝐴 ) ) )
6 hvsub0 ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 0ℎ ) = 𝐴 )
7 6 fveq2d ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝐴 −ℎ 0ℎ ) ) = ( normℎ ‘ 𝐴 ) )
8 3 5 7 3eqtr3d ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( - 1 ·ℎ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) )