Theorem nmf

Description: The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	|- X = ( Base ` G )
	nmf.n	|- N = ( norm ` G )
Assertion	nmf	|- ( G e. NrmGrp -> N : X --> RR )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	|- X = ( Base ` G )
2		nmf.n	|- N = ( norm ` G )
3		ngpgrp	|- ( G e. NrmGrp -> G e. Grp )
4		eqid	|- ( ( dist ` G ) |` ( X X. X ) ) = ( ( dist ` G ) |` ( X X. X ) )
5	1 4	ngpmet	|- ( G e. NrmGrp -> ( ( dist ` G ) |` ( X X. X ) ) e. ( Met ` X ) )
6		eqid	|- ( dist ` G ) = ( dist ` G )
7	2 1 6 4	nmf2	|- ( ( G e. Grp /\ ( ( dist ` G ) |` ( X X. X ) ) e. ( Met ` X ) ) -> N : X --> RR )
8	3 5 7	syl2anc	|- ( G e. NrmGrp -> N : X --> RR )