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