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 𝐾 ) )