Metamath Proof Explorer

Theorem tcphval

Description: Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
tcphval.v 
|- V = ( Base ` W )
tcphval.h 
|- ., = ( .i ` W )
Assertion tcphval 
|- G = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphval.v 
 |-  V = ( Base ` W )
3 tcphval.h 
 |-  ., = ( .i ` W )
4 id 
 |-  ( w = W -> w = W )
5 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
6 5 2 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
7 fveq2 
 |-  ( w = W -> ( .i ` w ) = ( .i ` W ) )
8 7 3 eqtr4di 
 |-  ( w = W -> ( .i ` w ) = ., )
9 8 oveqd 
 |-  ( w = W -> ( x ( .i ` w ) x ) = ( x ., x ) )
10 9 fveq2d 
 |-  ( w = W -> ( sqrt ` ( x ( .i ` w ) x ) ) = ( sqrt ` ( x ., x ) ) )
11 6 10 mpteq12dv 
 |-  ( w = W -> ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
12 4 11 oveq12d 
 |-  ( w = W -> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) )
13 df-tcph 
 |-  toCPreHil = ( w e. _V |-> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) )
14 ovex 
 |-  ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) e. _V
15 12 13 14 fvmpt 
 |-  ( W e. _V -> ( toCPreHil ` W ) = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) )
16 fvprc 
 |-  ( -. W e. _V -> ( toCPreHil ` W ) = (/) )
17 reldmtng 
 |-  Rel dom toNrmGrp
18 17 ovprc1 
 |-  ( -. W e. _V -> ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) = (/) )
19 16 18 eqtr4d 
 |-  ( -. W e. _V -> ( toCPreHil ` W ) = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) )
20 15 19 pm2.61i 
 |-  ( toCPreHil ` W ) = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
21 1 20 eqtri 
 |-  G = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )