Theorem tchnmfval

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	tchnmfval	|- ( W e. Grp -> N = ( x e. V |-> ( 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		eqid	|- ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) )
6		fvrn0	|- ( sqrt ` ( x ., x ) ) e. ( ran sqrt u. { (/) } )
7	6	a1i	|- ( x e. V -> ( sqrt ` ( x ., x ) ) e. ( ran sqrt u. { (/) } ) )
8	5 7	fmpti	|- ( x e. V |-> ( sqrt ` ( x ., x ) ) ) : V --> ( ran sqrt u. { (/) } )
9	1 3 4	tcphval	|- G = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
10		cnex	|- CC e. _V
11		sqrtf	|- sqrt : CC --> CC
12		frn	|- ( sqrt : CC --> CC -> ran sqrt C_ CC )
13	11 12	ax-mp	|- ran sqrt C_ CC
14	10 13	ssexi	|- ran sqrt e. _V
15		p0ex	|- { (/) } e. _V
16	14 15	unex	|- ( ran sqrt u. { (/) } ) e. _V
17	9 3 16	tngnm	|- ( ( W e. Grp /\ ( x e. V |-> ( sqrt ` ( x ., x ) ) ) : V --> ( ran sqrt u. { (/) } ) ) -> ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( norm ` G ) )
18	8 17	mpan2	|- ( W e. Grp -> ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( norm ` G ) )
19	2 18	eqtr4id	|- ( W e. Grp -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )