Theorem nmcn

Description: The norm of a normed group is a continuous function. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmcn.n	|- N = ( norm ` G )
	nmcn.j	|- J = ( TopOpen ` G )
	nmcn.k	|- K = ( topGen ` ran (,) )
Assertion	nmcn	|- ( G e. NrmGrp -> N e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		nmcn.n	|- N = ( norm ` G )
2		nmcn.j	|- J = ( TopOpen ` G )
3		nmcn.k	|- K = ( topGen ` ran (,) )
4		eqid	|- ( Base ` G ) = ( Base ` G )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6		eqid	|- ( dist ` G ) = ( dist ` G )
7	1 4 5 6	nmfval	|- N = ( x e. ( Base ` G ) |-> ( x ( dist ` G ) ( 0g ` G ) ) )
8		ngpms	|- ( G e. NrmGrp -> G e. MetSp )
9		ngptps	|- ( G e. NrmGrp -> G e. TopSp )
10	4 2	istps	|- ( G e. TopSp <-> J e. ( TopOn ` ( Base ` G ) ) )
11	9 10	sylib	|- ( G e. NrmGrp -> J e. ( TopOn ` ( Base ` G ) ) )
12	11	cnmptid	|- ( G e. NrmGrp -> ( x e. ( Base ` G ) |-> x ) e. ( J Cn J ) )
13		ngpgrp	|- ( G e. NrmGrp -> G e. Grp )
14	4 5	grpidcl	|- ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
15	13 14	syl	|- ( G e. NrmGrp -> ( 0g ` G ) e. ( Base ` G ) )
16	11 11 15	cnmptc	|- ( G e. NrmGrp -> ( x e. ( Base ` G ) |-> ( 0g ` G ) ) e. ( J Cn J ) )
17	6 2 3 8 11 12 16	cnmpt1ds	|- ( G e. NrmGrp -> ( x e. ( Base ` G ) |-> ( x ( dist ` G ) ( 0g ` G ) ) ) e. ( J Cn K ) )
18	7 17	eqeltrid	|- ( G e. NrmGrp -> N e. ( J Cn K ) )