Metamath Proof Explorer


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 NrmGrp N 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 0 G = 0 G
6 eqid dist G = dist G
7 1 4 5 6 nmfval N = x Base G x dist G 0 G
8 ngpms G NrmGrp G MetSp
9 ngptps G NrmGrp G TopSp
10 4 2 istps G TopSp J TopOn Base G
11 9 10 sylib G NrmGrp J TopOn Base G
12 11 cnmptid G NrmGrp x Base G x J Cn J
13 ngpgrp G NrmGrp G Grp
14 4 5 grpidcl G Grp 0 G Base G
15 13 14 syl G NrmGrp 0 G Base G
16 11 11 15 cnmptc G NrmGrp x Base G 0 G J Cn J
17 6 2 3 8 11 12 16 cnmpt1ds G NrmGrp x Base G x dist G 0 G J Cn K
18 7 17 eqeltrid G NrmGrp N J Cn K