nmcn

Description: The norm of a normed group is a continuous function. (Contributed by Mario Carneiro, 4-Oct-2015)

Step	Hyp	Ref	Expression
1		nmcn.n	$⊢ N = norm (G)$
2		nmcn.j	$⊢ J = TopOpen (G)$
3		nmcn.k	$⊢ K = topGen (ran (.))$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5		eqid	$⊢ 0_{G} = 0_{G}$
6		eqid	$⊢ dist (G) = dist (G)$
7	1 4 5 6	nmfval	$⊢ N = (x \in {Base}_{G} ⟼ x dist (G) 0_{G})$
8		ngpms	$⊢ G \in NrmGrp \to G \in MetSp$
9		ngptps	$⊢ G \in NrmGrp \to G \in TopSp$
10	4 2	istps	$⊢ G \in TopSp \leftrightarrow J \in TopOn ({Base}_{G})$
11	9 10	sylib	$⊢ G \in NrmGrp \to J \in TopOn ({Base}_{G})$
12	11	cnmptid	$⊢ G \in NrmGrp \to (x \in {Base}_{G} ⟼ x) \in (J Cn J)$
13		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
14	4 5	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
15	13 14	syl	$⊢ G \in NrmGrp \to 0_{G} \in {Base}_{G}$
16	11 11 15	cnmptc	$⊢ G \in NrmGrp \to (x \in {Base}_{G} ⟼ 0_{G}) \in (J Cn J)$
17	6 2 3 8 11 12 16	cnmpt1ds	$⊢ G \in NrmGrp \to (x \in {Base}_{G} ⟼ x dist (G) 0_{G}) \in (J Cn K)$
18	7 17	eqeltrid	$⊢ G \in NrmGrp \to N \in (J Cn K)$

Metamath Proof Explorer