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

Metamath Proof Explorer

Theorem ipnm

Description: Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipid.1 
|- X = ( BaseSet ` U )
ipid.6 
|- N = ( normCV ` U )
ipid.7 
|- P = ( .iOLD ` U )
Assertion ipnm 
|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) = ( sqrt ` ( A P A ) ) )

Proof

Step Hyp Ref Expression
1 ipid.1 
 |-  X = ( BaseSet ` U )
2 ipid.6 
 |-  N = ( normCV ` U )
3 ipid.7 
 |-  P = ( .iOLD ` U )
4 1 2 3 ipidsq 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( N ` A ) ^ 2 ) )
5 4 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( sqrt ` ( A P A ) ) = ( sqrt ` ( ( N ` A ) ^ 2 ) ) )
6 1 2 nvcl 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )
7 1 2 nvge0 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) )
8 6 7 sqrtsqd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( sqrt ` ( ( N ` A ) ^ 2 ) ) = ( N ` A ) )
9 5 8 eqtr2d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) = ( sqrt ` ( A P A ) ) )