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

Metamath Proof Explorer

Theorem cphnm

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses nmsq.v 
|- V = ( Base ` W )
nmsq.h 
|- ., = ( .i ` W )
nmsq.n 
|- N = ( norm ` W )
Assertion cphnm 
|- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) = ( sqrt ` ( 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 cphnmfval 
 |-  ( W e. CPreHil -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
5 4 fveq1d 
 |-  ( W e. CPreHil -> ( N ` A ) = ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` A ) )
6 oveq12 
 |-  ( ( x = A /\ x = A ) -> ( x ., x ) = ( A ., A ) )
7 6 anidms 
 |-  ( x = A -> ( x ., x ) = ( A ., A ) )
8 7 fveq2d 
 |-  ( x = A -> ( sqrt ` ( x ., x ) ) = ( sqrt ` ( A ., A ) ) )
9 eqid 
 |-  ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) )
10 fvex 
 |-  ( sqrt ` ( A ., A ) ) e. _V
11 8 9 10 fvmpt 
 |-  ( A e. V -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` A ) = ( sqrt ` ( A ., A ) ) )
12 5 11 sylan9eq 
 |-  ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) = ( sqrt ` ( A ., A ) ) )