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 e. ~H -> ( normh ` ( -u 1 .h A ) ) = ( normh ` A ) )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	|- 0h e. ~H
2		normsub	|- ( ( 0h e. ~H /\ A e. ~H ) -> ( normh ` ( 0h -h A ) ) = ( normh ` ( A -h 0h ) ) )
3	1 2	mpan	|- ( A e. ~H -> ( normh ` ( 0h -h A ) ) = ( normh ` ( A -h 0h ) ) )
4		hv2neg	|- ( A e. ~H -> ( 0h -h A ) = ( -u 1 .h A ) )
5	4	fveq2d	|- ( A e. ~H -> ( normh ` ( 0h -h A ) ) = ( normh ` ( -u 1 .h A ) ) )
6		hvsub0	|- ( A e. ~H -> ( A -h 0h ) = A )
7	6	fveq2d	|- ( A e. ~H -> ( normh ` ( A -h 0h ) ) = ( normh ` A ) )
8	3 5 7	3eqtr3d	|- ( A e. ~H -> ( normh ` ( -u 1 .h A ) ) = ( normh ` A ) )