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

Metamath Proof Explorer

Theorem normsqi

Description: The square of a norm. (Contributed by NM, 21-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypothesis normcl.1 
|- A e. ~H
Assertion normsqi 
|- ( ( normh ` A ) ^ 2 ) = ( A .ih A )

Proof

Step Hyp Ref Expression
1 normcl.1 
 |-  A e. ~H
2 normval 
 |-  ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) )
3 1 2 ax-mp 
 |-  ( normh ` A ) = ( sqrt ` ( A .ih A ) )
4 3 oveq1i 
 |-  ( ( normh ` A ) ^ 2 ) = ( ( sqrt ` ( A .ih A ) ) ^ 2 )
5 hiidge0 
 |-  ( A e. ~H -> 0 <_ ( A .ih A ) )
6 1 5 ax-mp 
 |-  0 <_ ( A .ih A )
7 hiidrcl 
 |-  ( A e. ~H -> ( A .ih A ) e. RR )
8 1 7 ax-mp 
 |-  ( A .ih A ) e. RR
9 8 sqsqrti 
 |-  ( 0 <_ ( A .ih A ) -> ( ( sqrt ` ( A .ih A ) ) ^ 2 ) = ( A .ih A ) )
10 6 9 ax-mp 
 |-  ( ( sqrt ` ( A .ih A ) ) ^ 2 ) = ( A .ih A )
11 4 10 eqtri 
 |-  ( ( normh ` A ) ^ 2 ) = ( A .ih A )