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

Metamath Proof Explorer

Theorem ngnmcncn

Description: The norm of a normed group is a continuous function to CC . (Contributed by NM, 12-Aug-2007) (Revised by AV, 17-Oct-2021)

Ref Expression
Hypotheses nmcn.n ⊢ N = norm ⁡ G
nmcn.j ⊢ J = TopOpen ⁡ G
ngnmcncn.k ⊢ K = TopOpen ⁡ ℂ fld
Assertion ngnmcncn ⊢ G ∈ NrmGrp → N ∈ J Cn K

Proof

Step Hyp Ref Expression
1 nmcn.n ⊢ N = norm ⁡ G
2 nmcn.j ⊢ J = TopOpen ⁡ G
3 ngnmcncn.k ⊢ K = TopOpen ⁡ ℂ fld
4 3 cnfldtop ⊢ K ∈ Top
5 cnrest2r ⊢ K ∈ Top → J Cn K ↾ 𝑡 ℝ ⊆ J Cn K
6 4 5 ax-mp ⊢ J Cn K ↾ 𝑡 ℝ ⊆ J Cn K
7 3 tgioo2 ⊢ topGen ⁡ ran ⁡ . = K ↾ 𝑡 ℝ
8 7 eqcomi ⊢ K ↾ 𝑡 ℝ = topGen ⁡ ran ⁡ .
9 1 2 8 nmcn ⊢ G ∈ NrmGrp → N ∈ J Cn K ↾ 𝑡 ℝ
10 6 9 sselid ⊢ G ∈ NrmGrp → N ∈ J Cn K