snclseqg

Description: The coset of the closure of the identity is the closure of a point. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	snclseqg.x	$⊢ X = {Base}_{G}$
	snclseqg.j	$⊢ J = TopOpen (G)$
	snclseqg.z	$⊢ \underset{˙}{0} = 0_{G}$
	snclseqg.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
	snclseqg.s	$⊢ S = cls (J) (\{\underset{˙}{0}\})$
Assertion	snclseqg	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = cls (J) (\{A\})$

Proof

Step	Hyp	Ref	Expression
1		snclseqg.x	$⊢ X = {Base}_{G}$
2		snclseqg.j	$⊢ J = TopOpen (G)$
3		snclseqg.z	$⊢ \underset{˙}{0} = 0_{G}$
4		snclseqg.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
5		snclseqg.s	$⊢ S = cls (J) (\{\underset{˙}{0}\})$
6	5	imaeq2i	$⊢ (x \in X ⟼ A +_{G} x) [S] = (x \in X ⟼ A +_{G} x) [cls (J) (\{\underset{˙}{0}\})]$
7		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
8	7	adantr	$⊢ (G \in TopGrp \land A \in X) \to G \in Grp$
9	2 1	tgptopon	$⊢ G \in TopGrp \to J \in TopOn (X)$
10	9	adantr	$⊢ (G \in TopGrp \land A \in X) \to J \in TopOn (X)$
11		topontop	$⊢ J \in TopOn (X) \to J \in Top$
12	10 11	syl	$⊢ (G \in TopGrp \land A \in X) \to J \in Top$
13	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in X$
14	8 13	syl	$⊢ (G \in TopGrp \land A \in X) \to \underset{˙}{0} \in X$
15	14	snssd	$⊢ (G \in TopGrp \land A \in X) \to \{\underset{˙}{0}\} \subseteq X$
16		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
17	10 16	syl	$⊢ (G \in TopGrp \land A \in X) \to X = ⋃ J$
18	15 17	sseqtrd	$⊢ (G \in TopGrp \land A \in X) \to \{\underset{˙}{0}\} \subseteq ⋃ J$
19		eqid	$⊢ ⋃ J = ⋃ J$
20	19	clsss3	$⊢ (J \in Top \land \{\underset{˙}{0}\} \subseteq ⋃ J) \to cls (J) (\{\underset{˙}{0}\}) \subseteq ⋃ J$
21	12 18 20	syl2anc	$⊢ (G \in TopGrp \land A \in X) \to cls (J) (\{\underset{˙}{0}\}) \subseteq ⋃ J$
22	21 17	sseqtrrd	$⊢ (G \in TopGrp \land A \in X) \to cls (J) (\{\underset{˙}{0}\}) \subseteq X$
23	5 22	eqsstrid	$⊢ (G \in TopGrp \land A \in X) \to S \subseteq X$
24		simpr	$⊢ (G \in TopGrp \land A \in X) \to A \in X$
25		eqid	$⊢ +_{G} = +_{G}$
26	1 4 25	eqglact	$⊢ (G \in Grp \land S \subseteq X \land A \in X) \to [A] \underset{˙}{\sim} = (x \in X ⟼ A +_{G} x) [S]$
27	8 23 24 26	syl3anc	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = (x \in X ⟼ A +_{G} x) [S]$
28		eqid	$⊢ (x \in X ⟼ A +_{G} x) = (x \in X ⟼ A +_{G} x)$
29	28 1 25 2	tgplacthmeo	$⊢ (G \in TopGrp \land A \in X) \to (x \in X ⟼ A +_{G} x) \in (J Homeo J)$
30	19	hmeocls	$⊢ ((x \in X ⟼ A +_{G} x) \in (J Homeo J) \land \{\underset{˙}{0}\} \subseteq ⋃ J) \to cls (J) ((x \in X ⟼ A +_{G} x) [\{\underset{˙}{0}\}]) = (x \in X ⟼ A +_{G} x) [cls (J) (\{\underset{˙}{0}\})]$
31	29 18 30	syl2anc	$⊢ (G \in TopGrp \land A \in X) \to cls (J) ((x \in X ⟼ A +_{G} x) [\{\underset{˙}{0}\}]) = (x \in X ⟼ A +_{G} x) [cls (J) (\{\underset{˙}{0}\})]$
32	6 27 31	3eqtr4a	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = cls (J) ((x \in X ⟼ A +_{G} x) [\{\underset{˙}{0}\}])$
33		df-ima	$⊢ (x \in X ⟼ A +_{G} x) [\{\underset{˙}{0}\}] = ran ({(x \in X ⟼ A +_{G} x) ↾}_{\{\underset{˙}{0}\}})$
34	15	resmptd	$⊢ (G \in TopGrp \land A \in X) \to {(x \in X ⟼ A +_{G} x) ↾}_{\{\underset{˙}{0}\}} = (x \in \{\underset{˙}{0}\} ⟼ A +_{G} x)$
35	34	rneqd	$⊢ (G \in TopGrp \land A \in X) \to ran ({(x \in X ⟼ A +_{G} x) ↾}_{\{\underset{˙}{0}\}}) = ran (x \in \{\underset{˙}{0}\} ⟼ A +_{G} x)$
36	33 35	eqtrid	$⊢ (G \in TopGrp \land A \in X) \to (x \in X ⟼ A +_{G} x) [\{\underset{˙}{0}\}] = ran (x \in \{\underset{˙}{0}\} ⟼ A +_{G} x)$
37	3	fvexi	$⊢ \underset{˙}{0} \in V$
38		oveq2	$⊢ x = \underset{˙}{0} \to A +_{G} x = A +_{G} \underset{˙}{0}$
39	38	eqeq2d	$⊢ x = \underset{˙}{0} \to (y = A +_{G} x \leftrightarrow y = A +_{G} \underset{˙}{0})$
40	37 39	rexsn	$⊢ \exists x \in \{\underset{˙}{0}\} y = A +_{G} x \leftrightarrow y = A +_{G} \underset{˙}{0}$
41	1 25 3	grprid	$⊢ (G \in Grp \land A \in X) \to A +_{G} \underset{˙}{0} = A$
42	7 41	sylan	$⊢ (G \in TopGrp \land A \in X) \to A +_{G} \underset{˙}{0} = A$
43	42	eqeq2d	$⊢ (G \in TopGrp \land A \in X) \to (y = A +_{G} \underset{˙}{0} \leftrightarrow y = A)$
44	40 43	bitrid	$⊢ (G \in TopGrp \land A \in X) \to (\exists x \in \{\underset{˙}{0}\} y = A +_{G} x \leftrightarrow y = A)$
45	44	abbidv	$⊢ (G \in TopGrp \land A \in X) \to \{y \| \exists x \in \{\underset{˙}{0}\} y = A +_{G} x\} = \{y \| y = A\}$
46		eqid	$⊢ (x \in \{\underset{˙}{0}\} ⟼ A +_{G} x) = (x \in \{\underset{˙}{0}\} ⟼ A +_{G} x)$
47	46	rnmpt	$⊢ ran (x \in \{\underset{˙}{0}\} ⟼ A +_{G} x) = \{y \| \exists x \in \{\underset{˙}{0}\} y = A +_{G} x\}$
48		df-sn	$⊢ \{A\} = \{y \| y = A\}$
49	45 47 48	3eqtr4g	$⊢ (G \in TopGrp \land A \in X) \to ran (x \in \{\underset{˙}{0}\} ⟼ A +_{G} x) = \{A\}$
50	36 49	eqtrd	$⊢ (G \in TopGrp \land A \in X) \to (x \in X ⟼ A +_{G} x) [\{\underset{˙}{0}\}] = \{A\}$
51	50	fveq2d	$⊢ (G \in TopGrp \land A \in X) \to cls (J) ((x \in X ⟼ A +_{G} x) [\{\underset{˙}{0}\}]) = cls (J) (\{A\})$
52	32 51	eqtrd	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = cls (J) (\{A\})$

Metamath Proof Explorer

Theorem snclseqg

Proof