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 ) )