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	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)={norm}_{ℎ}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2		normsub	$$⊢\left(0_{ℎ}\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to {norm}_{ℎ}\left(0_{ℎ}{-}_{ℎ}A\right)={norm}_{ℎ}\left(A{-}_{ℎ}{0}_{ℎ}\right)$$
3	1 2	mpan	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(0_{ℎ}{-}_{ℎ}A\right)={norm}_{ℎ}\left(A{-}_{ℎ}{0}_{ℎ}\right)$$
4		hv2neg	$$⊢A\in \mathscr{H}\to 0_{ℎ}{-}_{ℎ}A=-1{\cdot }_{ℎ}A$$
5	4	fveq2d	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(0_{ℎ}{-}_{ℎ}A\right)={norm}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
6		hvsub0	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}{0}_{ℎ}=A$$
7	6	fveq2d	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A{-}_{ℎ}{0}_{ℎ}\right)={norm}_{ℎ}\left(A\right)$$
8	3 5 7	3eqtr3d	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)={norm}_{ℎ}\left(A\right)$$