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

Metamath Proof Explorer

Theorem cphtcphnm

Description: The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
cphtcphnm.n 
|- N = ( norm ` W )
Assertion cphtcphnm 
|- ( W e. CPreHil -> N = ( norm ` G ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 cphtcphnm.n 
 |-  N = ( norm ` W )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 eqid 
 |-  ( .i ` W ) = ( .i ` W )
5 3 4 2 cphnmfval 
 |-  ( W e. CPreHil -> N = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
6 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
7 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
8 eqid 
 |-  ( norm ` G ) = ( norm ` G )
9 1 8 3 4 tchnmfval 
 |-  ( W e. Grp -> ( norm ` G ) = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
10 6 7 9 3syl 
 |-  ( W e. CPreHil -> ( norm ` G ) = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
11 5 10 eqtr4d 
 |-  ( W e. CPreHil -> N = ( norm ` G ) )