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

Proof

Step	Hyp	Ref	Expression
1		nmcn.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
2		nmcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3		ngnmcncn.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
4	3	cnfldtop	⊢ 𝐾 ∈ Top
5		cnrest2r	⊢ ( 𝐾 ∈ Top → ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 ) )
6	4 5	ax-mp	⊢ ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 )
7	3	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ )
8	7	eqcomi	⊢ ( 𝐾 ↾t ℝ ) = ( topGen ‘ ran (,) )
9	1 2 8	nmcn	⊢ ( 𝐺 ∈ NrmGrp → 𝑁 ∈ ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) )
10	6 9	sseldi	⊢ ( 𝐺 ∈ NrmGrp → 𝑁 ∈ ( 𝐽 Cn 𝐾 ) )