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

Metamath Proof Explorer

Theorem nmsq

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. Equation I4 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses nmsq.v 
|- V = ( Base ` W )
nmsq.h 
|- ., = ( .i ` W )
nmsq.n 
|- N = ( norm ` W )
Assertion nmsq 
|- ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )

Proof

Step Hyp Ref Expression
1 nmsq.v 
 |-  V = ( Base ` W )
2 nmsq.h 
 |-  ., = ( .i ` W )
3 nmsq.n 
 |-  N = ( norm ` W )
4 1 2 3 cphnm 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) = ( sqrt ` ( A ., A ) ) )
5 4 oveq1d 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( ( sqrt ` ( A ., A ) ) ^ 2 ) )
6 1 2 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ A e. V ) -> ( A ., A ) e. CC )
7 6 3anidm23 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( A ., A ) e. CC )
8 7 sqsqrtd 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( ( sqrt ` ( A ., A ) ) ^ 2 ) = ( A ., A ) )
9 5 8 eqtrd 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )