cldsubg

Description: A subgroup of finite index is closed iff it is open. (Contributed by Mario Carneiro, 20-Sep-2015)

	Ref	Expression
Hypotheses	subgntr.h	$⊢ J = TopOpen (G)$
	cldsubg.1	$⊢ R = G ~_{QG} S$
	cldsubg.2	$⊢ X = {Base}_{G}$
Assertion	cldsubg	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \to (S \in Clsd (J) \leftrightarrow S \in J)$

Proof

Step	Hyp	Ref	Expression
1		subgntr.h	$⊢ J = TopOpen (G)$
2		cldsubg.1	$⊢ R = G ~_{QG} S$
3		cldsubg.2	$⊢ X = {Base}_{G}$
4		simpl1	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to G \in TopGrp$
5	1 3	tgptopon	$⊢ G \in TopGrp \to J \in TopOn (X)$
6	4 5	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to J \in TopOn (X)$
7		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
8	6 7	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to X = ⋃ J$
9	8	difeq1d	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to X ∖ ⋃ ((X / R) ∖ \{S\}) = ⋃ J ∖ ⋃ ((X / R) ∖ \{S\})$
10		simpl2	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to S \in SubGrp (G)$
11		unisng	$⊢ S \in SubGrp (G) \to ⋃ \{S\} = S$
12	10 11	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ \{S\} = S$
13	12	uneq2d	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \cup ⋃ \{S\} = ⋃ ((X / R) ∖ \{S\}) \cup S$
14		uniun	$⊢ ⋃ (((X / R) ∖ \{S\}) \cup \{S\}) = ⋃ ((X / R) ∖ \{S\}) \cup ⋃ \{S\}$
15		undif1	$⊢ ((X / R) ∖ \{S\}) \cup \{S\} = (X / R) \cup \{S\}$
16		eqid	$⊢ 0_{G} = 0_{G}$
17	3 2 16	eqgid	$⊢ S \in SubGrp (G) \to [0_{G}] R = S$
18	10 17	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to [0_{G}] R = S$
19	2	ovexi	$⊢ R \in V$
20		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
21	4 20	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to G \in Grp$
22	3 16	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
23	21 22	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to 0_{G} \in X$
24		ecelqsw	$⊢ (R \in V \land 0_{G} \in X) \to [0_{G}] R \in (X / R)$
25	19 23 24	sylancr	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to [0_{G}] R \in (X / R)$
26	18 25	eqeltrrd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to S \in (X / R)$
27	26	snssd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to \{S\} \subseteq X / R$
28		ssequn2	$⊢ \{S\} \subseteq X / R \leftrightarrow (X / R) \cup \{S\} = X / R$
29	27 28	sylib	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (X / R) \cup \{S\} = X / R$
30	15 29	eqtrid	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ((X / R) ∖ \{S\}) \cup \{S\} = X / R$
31	30	unieqd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ (((X / R) ∖ \{S\}) \cup \{S\}) = ⋃ (X / R)$
32	3 2	eqger	$⊢ S \in SubGrp (G) \to R Er X$
33	10 32	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to R Er X$
34	19	a1i	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to R \in V$
35	33 34	uniqs2	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ (X / R) = X$
36	31 35	eqtrd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ (((X / R) ∖ \{S\}) \cup \{S\}) = X$
37	14 36	eqtr3id	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \cup ⋃ \{S\} = X$
38	13 37	eqtr3d	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \cup S = X$
39		difss	$⊢ (X / R) ∖ \{S\} \subseteq X / R$
40	39	unissi	$⊢ ⋃ ((X / R) ∖ \{S\}) \subseteq ⋃ (X / R)$
41	40 35	sseqtrid	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \subseteq X$
42		df-ne	$⊢ x \neq S \leftrightarrow \neg x = S$
43	33	adantr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land x \in (X / R)) \to R Er X$
44		simpr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land x \in (X / R)) \to x \in (X / R)$
45	26	adantr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land x \in (X / R)) \to S \in (X / R)$
46	43 44 45	qsdisj	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land x \in (X / R)) \to (x = S \lor x \cap S = \emptyset)$
47	46	ord	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land x \in (X / R)) \to (\neg x = S \to x \cap S = \emptyset)$
48		disj2	$⊢ x \cap S = \emptyset \leftrightarrow x \subseteq V ∖ S$
49	47 48	imbitrdi	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land x \in (X / R)) \to (\neg x = S \to x \subseteq V ∖ S)$
50	42 49	biimtrid	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land x \in (X / R)) \to (x \neq S \to x \subseteq V ∖ S)$
51	50	expimpd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ((x \in (X / R) \land x \neq S) \to x \subseteq V ∖ S)$
52		eldifsn	$⊢ x \in ((X / R) ∖ \{S\}) \leftrightarrow (x \in (X / R) \land x \neq S)$
53		velpw	$⊢ x \in 𝒫 (V ∖ S) \leftrightarrow x \subseteq V ∖ S$
54	51 52 53	3imtr4g	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (x \in ((X / R) ∖ \{S\}) \to x \in 𝒫 (V ∖ S))$
55	54	ssrdv	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (X / R) ∖ \{S\} \subseteq 𝒫 (V ∖ S)$
56		sspwuni	$⊢ (X / R) ∖ \{S\} \subseteq 𝒫 (V ∖ S) \leftrightarrow ⋃ ((X / R) ∖ \{S\}) \subseteq V ∖ S$
57	55 56	sylib	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \subseteq V ∖ S$
58		disj2	$⊢ ⋃ ((X / R) ∖ \{S\}) \cap S = \emptyset \leftrightarrow ⋃ ((X / R) ∖ \{S\}) \subseteq V ∖ S$
59	57 58	sylibr	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \cap S = \emptyset$
60		uneqdifeq	$⊢ (⋃ ((X / R) ∖ \{S\}) \subseteq X \land ⋃ ((X / R) ∖ \{S\}) \cap S = \emptyset) \to (⋃ ((X / R) ∖ \{S\}) \cup S = X \leftrightarrow X ∖ ⋃ ((X / R) ∖ \{S\}) = S)$
61	41 59 60	syl2anc	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (⋃ ((X / R) ∖ \{S\}) \cup S = X \leftrightarrow X ∖ ⋃ ((X / R) ∖ \{S\}) = S)$
62	38 61	mpbid	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to X ∖ ⋃ ((X / R) ∖ \{S\}) = S$
63	9 62	eqtr3d	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ J ∖ ⋃ ((X / R) ∖ \{S\}) = S$
64		topontop	$⊢ J \in TopOn (X) \to J \in Top$
65	6 64	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to J \in Top$
66		simpl3	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to X / R \in Fin$
67		diffi	$⊢ X / R \in Fin \to (X / R) ∖ \{S\} \in Fin$
68	66 67	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (X / R) ∖ \{S\} \in Fin$
69		vex	$⊢ x \in V$
70	69	elqs	$⊢ x \in (X / R) \leftrightarrow \exists y \in X x = [y] R$
71		simpll2	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to S \in SubGrp (G)$
72		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
73	71 72	syl	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to G \in Grp$
74	3	subgss	$⊢ S \in SubGrp (G) \to S \subseteq X$
75	10 74	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to S \subseteq X$
76	75	adantr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to S \subseteq X$
77		simpr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to y \in X$
78		eqid	$⊢ +_{G} = +_{G}$
79	3 2 78	eqglact	$⊢ (G \in Grp \land S \subseteq X \land y \in X) \to [y] R = (z \in X ⟼ y +_{G} z) [S]$
80	73 76 77 79	syl3anc	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to [y] R = (z \in X ⟼ y +_{G} z) [S]$
81		simplr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to S \in Clsd (J)$
82		eqid	$⊢ (z \in X ⟼ y +_{G} z) = (z \in X ⟼ y +_{G} z)$
83	82 3 78 1	tgplacthmeo	$⊢ (G \in TopGrp \land y \in X) \to (z \in X ⟼ y +_{G} z) \in (J Homeo J)$
84	4 83	sylan	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to (z \in X ⟼ y +_{G} z) \in (J Homeo J)$
85	75 8	sseqtrd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to S \subseteq ⋃ J$
86	85	adantr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to S \subseteq ⋃ J$
87		eqid	$⊢ ⋃ J = ⋃ J$
88	87	hmeocld	$⊢ ((z \in X ⟼ y +_{G} z) \in (J Homeo J) \land S \subseteq ⋃ J) \to (S \in Clsd (J) \leftrightarrow (z \in X ⟼ y +_{G} z) [S] \in Clsd (J))$
89	84 86 88	syl2anc	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to (S \in Clsd (J) \leftrightarrow (z \in X ⟼ y +_{G} z) [S] \in Clsd (J))$
90	81 89	mpbid	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to (z \in X ⟼ y +_{G} z) [S] \in Clsd (J)$
91	80 90	eqeltrd	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to [y] R \in Clsd (J)$
92		eleq1	$⊢ x = [y] R \to (x \in Clsd (J) \leftrightarrow [y] R \in Clsd (J))$
93	91 92	syl5ibrcom	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \land y \in X) \to (x = [y] R \to x \in Clsd (J))$
94	93	rexlimdva	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (\exists y \in X x = [y] R \to x \in Clsd (J))$
95	70 94	biimtrid	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (x \in (X / R) \to x \in Clsd (J))$
96	95	ssrdv	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to X / R \subseteq Clsd (J)$
97	96	ssdifssd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to (X / R) ∖ \{S\} \subseteq Clsd (J)$
98	87	unicld	$⊢ (J \in Top \land (X / R) ∖ \{S\} \in Fin \land (X / R) ∖ \{S\} \subseteq Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \in Clsd (J)$
99	65 68 97 98	syl3anc	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ ((X / R) ∖ \{S\}) \in Clsd (J)$
100	87	cldopn	$⊢ ⋃ ((X / R) ∖ \{S\}) \in Clsd (J) \to ⋃ J ∖ ⋃ ((X / R) ∖ \{S\}) \in J$
101	99 100	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to ⋃ J ∖ ⋃ ((X / R) ∖ \{S\}) \in J$
102	63 101	eqeltrrd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \land S \in Clsd (J)) \to S \in J$
103	102	ex	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \to (S \in Clsd (J) \to S \in J)$
104	1	opnsubg	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to S \in Clsd (J)$
105	104	3expia	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to (S \in J \to S \in Clsd (J))$
106	105	3adant3	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \to (S \in J \to S \in Clsd (J))$
107	103 106	impbid	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land X / R \in Fin) \to (S \in Clsd (J) \leftrightarrow S \in J)$

Metamath Proof Explorer

Theorem cldsubg

Proof