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 ⊢ 𝑁 = ( norm ‘ 𝐺 )
nmcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
nmcn.k ⊢ 𝐾 = ( topGen ‘ ran (,) )
Assertion nmcn ( 𝐺 ∈ NrmGrp → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 nmcn.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
2 nmcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 nmcn.k ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
7 1 4 5 6 nmfval ⊢ 𝑁 = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
8 ngpms ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
9 ngptps ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp )
10 4 2 istps ⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
11 9 10 sylib ⊢ ( 𝐺 ∈ NrmGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
12 11 cnmptid ⊢ ( 𝐺 ∈ NrmGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
13 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
14 4 5 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
15 13 14 syl ⊢ ( 𝐺 ∈ NrmGrp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
16 11 11 15 cnmptc ⊢ ( 𝐺 ∈ NrmGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 0g ‘ 𝐺 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
17 6 2 3 8 11 12 16 cnmpt1ds ⊢ ( 𝐺 ∈ NrmGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( dist ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) ∈ ( 𝐽 Cn 𝐾 ) )
18 7 17 eqeltrid ⊢ ( 𝐺 ∈ NrmGrp → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) )