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

Metamath Proof Explorer

Theorem tcphnmval

Description: The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
tcphnmval.n 
|- N = ( norm ` G )
tcphnmval.v 
|- V = ( Base ` W )
tcphnmval.h 
|- ., = ( .i ` W )
Assertion tcphnmval 
|- ( ( W e. Grp /\ X e. V ) -> ( N ` X ) = ( sqrt ` ( X ., X ) ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphnmval.n 
 |-  N = ( norm ` G )
3 tcphnmval.v 
 |-  V = ( Base ` W )
4 tcphnmval.h 
 |-  ., = ( .i ` W )
5 1 2 3 4 tchnmfval 
 |-  ( W e. Grp -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
6 5 fveq1d 
 |-  ( W e. Grp -> ( N ` X ) = ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` X ) )
7 oveq12 
 |-  ( ( x = X /\ x = X ) -> ( x ., x ) = ( X ., X ) )
8 7 anidms 
 |-  ( x = X -> ( x ., x ) = ( X ., X ) )
9 8 fveq2d 
 |-  ( x = X -> ( sqrt ` ( x ., x ) ) = ( sqrt ` ( X ., X ) ) )
10 eqid 
 |-  ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) )
11 fvex 
 |-  ( sqrt ` ( X ., X ) ) e. _V
12 9 10 11 fvmpt 
 |-  ( X e. V -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` X ) = ( sqrt ` ( X ., X ) ) )
13 6 12 sylan9eq 
 |-  ( ( W e. Grp /\ X e. V ) -> ( N ` X ) = ( sqrt ` ( X ., X ) ) )