This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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