clssubg

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

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

Proof

Step	Hyp	Ref	Expression
1		subgntr.h	$⊢ J = TopOpen (G)$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3	1 2	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
4	3	adantr	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to J \in TopOn ({Base}_{G})$
5		topontop	$⊢ J \in TopOn ({Base}_{G}) \to J \in Top$
6	4 5	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to J \in Top$
7	2	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
8	7	adantl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \subseteq {Base}_{G}$
9		toponuni	$⊢ J \in TopOn ({Base}_{G}) \to {Base}_{G} = ⋃ J$
10	4 9	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {Base}_{G} = ⋃ J$
11	8 10	sseqtrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \subseteq ⋃ J$
12		eqid	$⊢ ⋃ J = ⋃ J$
13	12	clsss3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) \subseteq ⋃ J$
14	6 11 13	syl2anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J) (S) \subseteq ⋃ J$
15	14 10	sseqtrrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J) (S) \subseteq {Base}_{G}$
16	12	sscls	$⊢ (J \in Top \land S \subseteq ⋃ J) \to S \subseteq cls (J) (S)$
17	6 11 16	syl2anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \subseteq cls (J) (S)$
18		eqid	$⊢ 0_{G} = 0_{G}$
19	18	subg0cl	$⊢ S \in SubGrp (G) \to 0_{G} \in S$
20	19	adantl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to 0_{G} \in S$
21	20	ne0d	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \neq \emptyset$
22		ssn0	$⊢ (S \subseteq cls (J) (S) \land S \neq \emptyset) \to cls (J) (S) \neq \emptyset$
23	17 21 22	syl2anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J) (S) \neq \emptyset$
24		df-ov	$⊢ x -_{G} y = -_{G} (⟨x, y⟩)$
25		opelxpi	$⊢ (x \in cls (J) (S) \land y \in cls (J) (S)) \to ⟨x, y⟩ \in (cls (J) (S) \times cls (J) (S))$
26		txcls	$⊢ ((J \in TopOn ({Base}_{G}) \land J \in TopOn ({Base}_{G})) \land (S \subseteq {Base}_{G} \land S \subseteq {Base}_{G})) \to cls (J \times_{t} J) (S \times S) = cls (J) (S) \times cls (J) (S)$
27	4 4 8 8 26	syl22anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J \times_{t} J) (S \times S) = cls (J) (S) \times cls (J) (S)$
28		txtopon	$⊢ (J \in TopOn ({Base}_{G}) \land J \in TopOn ({Base}_{G})) \to J \times_{t} J \in TopOn ({Base}_{G} \times {Base}_{G})$
29	4 4 28	syl2anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to J \times_{t} J \in TopOn ({Base}_{G} \times {Base}_{G})$
30		topontop	$⊢ J \times_{t} J \in TopOn ({Base}_{G} \times {Base}_{G}) \to J \times_{t} J \in Top$
31	29 30	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to J \times_{t} J \in Top$
32		cnvimass	$⊢ {-_{G}}^{-1} [S] \subseteq dom -_{G}$
33		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
34	33	adantr	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to G \in Grp$
35		eqid	$⊢ -_{G} = -_{G}$
36	2 35	grpsubf	$⊢ G \in Grp \to -_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G}$
37	34 36	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to -_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G}$
38	32 37	fssdm	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {-_{G}}^{-1} [S] \subseteq {Base}_{G} \times {Base}_{G}$
39		toponuni	$⊢ J \times_{t} J \in TopOn ({Base}_{G} \times {Base}_{G}) \to {Base}_{G} \times {Base}_{G} = ⋃ (J \times_{t} J)$
40	29 39	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {Base}_{G} \times {Base}_{G} = ⋃ (J \times_{t} J)$
41	38 40	sseqtrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {-_{G}}^{-1} [S] \subseteq ⋃ (J \times_{t} J)$
42	35	subgsubcl	$⊢ (S \in SubGrp (G) \land x \in S \land y \in S) \to x -_{G} y \in S$
43	42	3expb	$⊢ (S \in SubGrp (G) \land (x \in S \land y \in S)) \to x -_{G} y \in S$
44	43	ralrimivva	$⊢ S \in SubGrp (G) \to \forall x \in S \forall y \in S x -_{G} y \in S$
45		fveq2	$⊢ z = ⟨x, y⟩ \to -_{G} (z) = -_{G} (⟨x, y⟩)$
46	45 24	eqtr4di	$⊢ z = ⟨x, y⟩ \to -_{G} (z) = x -_{G} y$
47	46	eleq1d	$⊢ z = ⟨x, y⟩ \to (-_{G} (z) \in S \leftrightarrow x -_{G} y \in S)$
48	47	ralxp	$⊢ \forall z \in (S \times S) -_{G} (z) \in S \leftrightarrow \forall x \in S \forall y \in S x -_{G} y \in S$
49	44 48	sylibr	$⊢ S \in SubGrp (G) \to \forall z \in (S \times S) -_{G} (z) \in S$
50	49	adantl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to \forall z \in (S \times S) -_{G} (z) \in S$
51	37	ffund	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to Fun -_{G}$
52		xpss12	$⊢ (S \subseteq {Base}_{G} \land S \subseteq {Base}_{G}) \to S \times S \subseteq {Base}_{G} \times {Base}_{G}$
53	8 8 52	syl2anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \times S \subseteq {Base}_{G} \times {Base}_{G}$
54	37	fdmd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to dom -_{G} = {Base}_{G} \times {Base}_{G}$
55	53 54	sseqtrrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \times S \subseteq dom -_{G}$
56		funimass5	$⊢ (Fun -_{G} \land S \times S \subseteq dom -_{G}) \to (S \times S \subseteq {-_{G}}^{-1} [S] \leftrightarrow \forall z \in (S \times S) -_{G} (z) \in S)$
57	51 55 56	syl2anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to (S \times S \subseteq {-_{G}}^{-1} [S] \leftrightarrow \forall z \in (S \times S) -_{G} (z) \in S)$
58	50 57	mpbird	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \times S \subseteq {-_{G}}^{-1} [S]$
59		eqid	$⊢ ⋃ (J \times_{t} J) = ⋃ (J \times_{t} J)$
60	59	clsss	$⊢ (J \times_{t} J \in Top \land {-_{G}}^{-1} [S] \subseteq ⋃ (J \times_{t} J) \land S \times S \subseteq {-_{G}}^{-1} [S]) \to cls (J \times_{t} J) (S \times S) \subseteq cls (J \times_{t} J) ({-_{G}}^{-1} [S])$
61	31 41 58 60	syl3anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J \times_{t} J) (S \times S) \subseteq cls (J \times_{t} J) ({-_{G}}^{-1} [S])$
62	1 35	tgpsubcn	$⊢ G \in TopGrp \to -_{G} \in ((J \times_{t} J) Cn J)$
63	62	adantr	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to -_{G} \in ((J \times_{t} J) Cn J)$
64	12	cncls2i	$⊢ (-_{G} \in ((J \times_{t} J) Cn J) \land S \subseteq ⋃ J) \to cls (J \times_{t} J) ({-_{G}}^{-1} [S]) \subseteq {-_{G}}^{-1} [cls (J) (S)]$
65	63 11 64	syl2anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J \times_{t} J) ({-_{G}}^{-1} [S]) \subseteq {-_{G}}^{-1} [cls (J) (S)]$
66	61 65	sstrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J \times_{t} J) (S \times S) \subseteq {-_{G}}^{-1} [cls (J) (S)]$
67	27 66	eqsstrrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J) (S) \times cls (J) (S) \subseteq {-_{G}}^{-1} [cls (J) (S)]$
68	67	sselda	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land ⟨x, y⟩ \in (cls (J) (S) \times cls (J) (S))) \to ⟨x, y⟩ \in {-_{G}}^{-1} [cls (J) (S)]$
69	25 68	sylan2	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land (x \in cls (J) (S) \land y \in cls (J) (S))) \to ⟨x, y⟩ \in {-_{G}}^{-1} [cls (J) (S)]$
70	33	ad2antrr	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land (x \in cls (J) (S) \land y \in cls (J) (S))) \to G \in Grp$
71		ffn	$⊢ -_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G} \to -_{G} Fn ({Base}_{G} \times {Base}_{G})$
72		elpreima	$⊢ -_{G} Fn ({Base}_{G} \times {Base}_{G}) \to (⟨x, y⟩ \in {-_{G}}^{-1} [cls (J) (S)] \leftrightarrow (⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \land -_{G} (⟨x, y⟩) \in cls (J) (S)))$
73	70 36 71 72	4syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land (x \in cls (J) (S) \land y \in cls (J) (S))) \to (⟨x, y⟩ \in {-_{G}}^{-1} [cls (J) (S)] \leftrightarrow (⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \land -_{G} (⟨x, y⟩) \in cls (J) (S)))$
74	69 73	mpbid	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land (x \in cls (J) (S) \land y \in cls (J) (S))) \to (⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \land -_{G} (⟨x, y⟩) \in cls (J) (S))$
75	74	simprd	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land (x \in cls (J) (S) \land y \in cls (J) (S))) \to -_{G} (⟨x, y⟩) \in cls (J) (S)$
76	24 75	eqeltrid	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land (x \in cls (J) (S) \land y \in cls (J) (S))) \to x -_{G} y \in cls (J) (S)$
77	76	ralrimivva	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to \forall x \in cls (J) (S) \forall y \in cls (J) (S) x -_{G} y \in cls (J) (S)$
78	2 35	issubg4	$⊢ G \in Grp \to (cls (J) (S) \in SubGrp (G) \leftrightarrow (cls (J) (S) \subseteq {Base}_{G} \land cls (J) (S) \neq \emptyset \land \forall x \in cls (J) (S) \forall y \in cls (J) (S) x -_{G} y \in cls (J) (S)))$
79	34 78	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to (cls (J) (S) \in SubGrp (G) \leftrightarrow (cls (J) (S) \subseteq {Base}_{G} \land cls (J) (S) \neq \emptyset \land \forall x \in cls (J) (S) \forall y \in cls (J) (S) x -_{G} y \in cls (J) (S)))$
80	15 23 77 79	mpbir3and	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to cls (J) (S) \in SubGrp (G)$

Metamath Proof Explorer

Theorem clssubg

Proof