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 
|- ( 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 ) )