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ℎ ‘ 𝐴 ) )