clsnsg

Description: The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

		Ref	Expression
	Hypothesis	subgntr.h	$⊢ J = TopOpen (G)$
	Assertion	clsnsg	$⊢ (G \in TopGrp \land S \in NrmSGrp (G)) \to cls (J) (S) \in NrmSGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		subgntr.h	$⊢ J = TopOpen (G)$
2		nsgsubg	$⊢ S \in NrmSGrp (G) \to S \in SubGrp (G)$
3	1	clssubg	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J) (S) \in SubGrp (G)$
4	2 3	sylan2	$⊢ (G \in TopGrp \land S \in NrmSGrp (G)) \to cls (J) (S) \in SubGrp (G)$
5		df-ima	$⊢ (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [cls (J) (S)] = ran ({(y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) ↾}_{cls (J) (S)})$
6		eqid	$⊢ {Base}_{G} = {Base}_{G}$
7	1 6	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
8	7	ad2antrr	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to J \in TopOn ({Base}_{G})$
9		topontop	$⊢ J \in TopOn ({Base}_{G}) \to J \in Top$
10	8 9	syl	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to J \in Top$
11	2	ad2antlr	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to S \in SubGrp (G)$
12	6	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
13	11 12	syl	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to S \subseteq {Base}_{G}$
14		toponuni	$⊢ J \in TopOn ({Base}_{G}) \to {Base}_{G} = ⋃ J$
15	8 14	syl	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to {Base}_{G} = ⋃ J$
16	13 15	sseqtrd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to S \subseteq ⋃ J$
17		eqid	$⊢ ⋃ J = ⋃ J$
18	17	clsss3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) \subseteq ⋃ J$
19	10 16 18	syl2anc	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to cls (J) (S) \subseteq ⋃ J$
20	19 15	sseqtrrd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to cls (J) (S) \subseteq {Base}_{G}$
21	20	resmptd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to {(y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) ↾}_{cls (J) (S)} = (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x)$
22	21	rneqd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to ran ({(y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) ↾}_{cls (J) (S)}) = ran (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x)$
23	5 22	syl5eq	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [cls (J) (S)] = ran (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x)$
24		eqid	$⊢ +_{G} = +_{G}$
25		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
26	25	ad2antrr	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to G \in TopMnd$
27		simpr	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to x \in {Base}_{G}$
28	8 8 27	cnmptc	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ x) \in (J Cn J)$
29	8	cnmptid	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ y) \in (J Cn J)$
30	1 24 26 8 28 29	cnmpt1plusg	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ x +_{G} y) \in (J Cn J)$
31		eqid	$⊢ -_{G} = -_{G}$
32	1 31	tgpsubcn	$⊢ G \in TopGrp \to -_{G} \in ((J \times_{t} J) Cn J)$
33	32	ad2antrr	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to -_{G} \in ((J \times_{t} J) Cn J)$
34	8 30 28 33	cnmpt12f	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) \in (J Cn J)$
35	17	cnclsi	$⊢ ((y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) \in (J Cn J) \land S \subseteq ⋃ J) \to (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [cls (J) (S)] \subseteq cls (J) ((y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S])$
36	34 16 35	syl2anc	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [cls (J) (S)] \subseteq cls (J) ((y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S])$
37		df-ima	$⊢ (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S] = ran ({(y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) ↾}_{S})$
38	13	resmptd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to {(y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) ↾}_{S} = (y \in S ⟼ (x +_{G} y) -_{G} x)$
39	38	rneqd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to ran ({(y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) ↾}_{S}) = ran (y \in S ⟼ (x +_{G} y) -_{G} x)$
40	37 39	syl5eq	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S] = ran (y \in S ⟼ (x +_{G} y) -_{G} x)$
41	6 24 31	nsgconj	$⊢ (S \in NrmSGrp (G) \land x \in {Base}_{G} \land y \in S) \to (x +_{G} y) -_{G} x \in S$
42	41	ad4ant234	$⊢ (((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \land y \in S) \to (x +_{G} y) -_{G} x \in S$
43	42	fmpttd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in S ⟼ (x +_{G} y) -_{G} x) : S ⟶ S$
44	43	frnd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to ran (y \in S ⟼ (x +_{G} y) -_{G} x) \subseteq S$
45	40 44	eqsstrd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S] \subseteq S$
46	17	clsss	$⊢ (J \in Top \land S \subseteq ⋃ J \land (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S] \subseteq S) \to cls (J) ((y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S]) \subseteq cls (J) (S)$
47	10 16 45 46	syl3anc	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to cls (J) ((y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [S]) \subseteq cls (J) (S)$
48	36 47	sstrd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ (x +_{G} y) -_{G} x) [cls (J) (S)] \subseteq cls (J) (S)$
49	23 48	eqsstrrd	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to ran (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) \subseteq cls (J) (S)$
50		ovex	$⊢ (x +_{G} y) -_{G} x \in V$
51		eqid	$⊢ (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) = (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x)$
52	50 51	fnmpti	$⊢ (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) Fn cls (J) (S)$
53		df-f	$⊢ (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) : cls (J) (S) ⟶ cls (J) (S) \leftrightarrow ((y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) Fn cls (J) (S) \land ran (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) \subseteq cls (J) (S))$
54	52 53	mpbiran	$⊢ (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) : cls (J) (S) ⟶ cls (J) (S) \leftrightarrow ran (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) \subseteq cls (J) (S)$
55	49 54	sylibr	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) : cls (J) (S) ⟶ cls (J) (S)$
56	51	fmpt	$⊢ \forall y \in cls (J) (S) (x +_{G} y) -_{G} x \in cls (J) (S) \leftrightarrow (y \in cls (J) (S) ⟼ (x +_{G} y) -_{G} x) : cls (J) (S) ⟶ cls (J) (S)$
57	55 56	sylibr	$⊢ ((G \in TopGrp \land S \in NrmSGrp (G)) \land x \in {Base}_{G}) \to \forall y \in cls (J) (S) (x +_{G} y) -_{G} x \in cls (J) (S)$
58	57	ralrimiva	$⊢ (G \in TopGrp \land S \in NrmSGrp (G)) \to \forall x \in {Base}_{G} \forall y \in cls (J) (S) (x +_{G} y) -_{G} x \in cls (J) (S)$
59	6 24 31	isnsg3	$⊢ cls (J) (S) \in NrmSGrp (G) \leftrightarrow (cls (J) (S) \in SubGrp (G) \land \forall x \in {Base}_{G} \forall y \in cls (J) (S) (x +_{G} y) -_{G} x \in cls (J) (S))$
60	4 58 59	sylanbrc	$⊢ (G \in TopGrp \land S \in NrmSGrp (G)) \to cls (J) (S) \in NrmSGrp (G)$

Metamath Proof Explorer

Theorem clsnsg

Proof