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 ` CCfld )
Assertion	ngnmcncn	|- ( 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		ngnmcncn.k	|- K = ( TopOpen ` CCfld )
4	3	cnfldtop	|- K e. Top
5		cnrest2r	|- ( K e. Top -> ( J Cn ( K |`t RR ) ) C_ ( J Cn K ) )
6	4 5	ax-mp	|- ( J Cn ( K |`t RR ) ) C_ ( J Cn K )
7	3	tgioo2	|- ( topGen ` ran (,) ) = ( K |`t RR )
8	7	eqcomi	|- ( K |`t RR ) = ( topGen ` ran (,) )
9	1 2 8	nmcn	|- ( G e. NrmGrp -> N e. ( J Cn ( K |`t RR ) ) )
10	6 9	sselid	|- ( G e. NrmGrp -> N e. ( J Cn K ) )