tgpconncompeqg

Description: The connected component containing A is the left coset of the identity component containing A . (Contributed by Mario Carneiro, 17-Sep-2015)

	Ref	Expression
Hypotheses	tgpconncomp.x	$⊢ X = {Base}_{G}$
	tgpconncomp.z	$⊢ \underset{˙}{0} = 0_{G}$
	tgpconncomp.j	$⊢ J = TopOpen (G)$
	tgpconncomp.s	$⊢ S = ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\}$
	tgpconncompeqg.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
Assertion	tgpconncompeqg	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$

Proof

Step	Hyp	Ref	Expression
1		tgpconncomp.x	$⊢ X = {Base}_{G}$
2		tgpconncomp.z	$⊢ \underset{˙}{0} = 0_{G}$
3		tgpconncomp.j	$⊢ J = TopOpen (G)$
4		tgpconncomp.s	$⊢ S = ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\}$
5		tgpconncompeqg.r	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
6		dfec2	$⊢ A \in X \to [A] \underset{˙}{\sim} = \{z \| A \underset{˙}{\sim} z\}$
7	6	adantl	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = \{z \| A \underset{˙}{\sim} z\}$
8		ssrab2	$⊢ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq 𝒫 X$
9		sspwuni	$⊢ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq 𝒫 X \leftrightarrow ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq X$
10	8 9	mpbi	$⊢ ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq X$
11	4 10	eqsstri	$⊢ S \subseteq X$
12	11	a1i	$⊢ (G \in TopGrp \land A \in X) \to S \subseteq X$
13		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
14		eqid	$⊢ +_{G} = +_{G}$
15	1 13 14 5	eqgval	$⊢ (G \in TopGrp \land S \subseteq X) \to (A \underset{˙}{\sim} z \leftrightarrow (A \in X \land z \in X \land {inv}_{g} (G) (A) +_{G} z \in S))$
16	12 15	syldan	$⊢ (G \in TopGrp \land A \in X) \to (A \underset{˙}{\sim} z \leftrightarrow (A \in X \land z \in X \land {inv}_{g} (G) (A) +_{G} z \in S))$
17		simp2	$⊢ (A \in X \land z \in X \land {inv}_{g} (G) (A) +_{G} z \in S) \to z \in X$
18	16 17	syl6bi	$⊢ (G \in TopGrp \land A \in X) \to (A \underset{˙}{\sim} z \to z \in X)$
19	18	abssdv	$⊢ (G \in TopGrp \land A \in X) \to \{z \| A \underset{˙}{\sim} z\} \subseteq X$
20	7 19	eqsstrd	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} \subseteq X$
21		simpr	$⊢ (G \in TopGrp \land A \in X) \to A \in X$
22		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
23	1 14 2 13	grplinv	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) +_{G} A = \underset{˙}{0}$
24	22 23	sylan	$⊢ (G \in TopGrp \land A \in X) \to {inv}_{g} (G) (A) +_{G} A = \underset{˙}{0}$
25	3 1	tgptopon	$⊢ G \in TopGrp \to J \in TopOn (X)$
26	25	adantr	$⊢ (G \in TopGrp \land A \in X) \to J \in TopOn (X)$
27	22	adantr	$⊢ (G \in TopGrp \land A \in X) \to G \in Grp$
28	1 2	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in X$
29	27 28	syl	$⊢ (G \in TopGrp \land A \in X) \to \underset{˙}{0} \in X$
30	4	conncompid	$⊢ (J \in TopOn (X) \land \underset{˙}{0} \in X) \to \underset{˙}{0} \in S$
31	26 29 30	syl2anc	$⊢ (G \in TopGrp \land A \in X) \to \underset{˙}{0} \in S$
32	24 31	eqeltrd	$⊢ (G \in TopGrp \land A \in X) \to {inv}_{g} (G) (A) +_{G} A \in S$
33	1 13 14 5	eqgval	$⊢ (G \in TopGrp \land S \subseteq X) \to (A \underset{˙}{\sim} A \leftrightarrow (A \in X \land A \in X \land {inv}_{g} (G) (A) +_{G} A \in S))$
34	12 33	syldan	$⊢ (G \in TopGrp \land A \in X) \to (A \underset{˙}{\sim} A \leftrightarrow (A \in X \land A \in X \land {inv}_{g} (G) (A) +_{G} A \in S))$
35	21 21 32 34	mpbir3and	$⊢ (G \in TopGrp \land A \in X) \to A \underset{˙}{\sim} A$
36		elecg	$⊢ (A \in X \land A \in X) \to (A \in [A] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{\sim} A)$
37	21 21 36	syl2anc	$⊢ (G \in TopGrp \land A \in X) \to (A \in [A] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{\sim} A)$
38	35 37	mpbird	$⊢ (G \in TopGrp \land A \in X) \to A \in [A] \underset{˙}{\sim}$
39	1 5 14	eqglact	$⊢ (G \in Grp \land S \subseteq X \land A \in X) \to [A] \underset{˙}{\sim} = (z \in X ⟼ A +_{G} z) [S]$
40	11 39	mp3an2	$⊢ (G \in Grp \land A \in X) \to [A] \underset{˙}{\sim} = (z \in X ⟼ A +_{G} z) [S]$
41	22 40	sylan	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = (z \in X ⟼ A +_{G} z) [S]$
42	41	oveq2d	$⊢ (G \in TopGrp \land A \in X) \to J ↾_{𝑡} [A] \underset{˙}{\sim} = J ↾_{𝑡} (z \in X ⟼ A +_{G} z) [S]$
43		eqid	$⊢ ⋃ J = ⋃ J$
44		eqid	$⊢ (z \in X ⟼ A +_{G} z) = (z \in X ⟼ A +_{G} z)$
45	44 1 14 3	tgplacthmeo	$⊢ (G \in TopGrp \land A \in X) \to (z \in X ⟼ A +_{G} z) \in (J Homeo J)$
46		hmeocn	$⊢ (z \in X ⟼ A +_{G} z) \in (J Homeo J) \to (z \in X ⟼ A +_{G} z) \in (J Cn J)$
47	45 46	syl	$⊢ (G \in TopGrp \land A \in X) \to (z \in X ⟼ A +_{G} z) \in (J Cn J)$
48		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
49	26 48	syl	$⊢ (G \in TopGrp \land A \in X) \to X = ⋃ J$
50	11 49	sseqtrid	$⊢ (G \in TopGrp \land A \in X) \to S \subseteq ⋃ J$
51	4	conncompconn	$⊢ (J \in TopOn (X) \land \underset{˙}{0} \in X) \to J ↾_{𝑡} S \in Conn$
52	26 29 51	syl2anc	$⊢ (G \in TopGrp \land A \in X) \to J ↾_{𝑡} S \in Conn$
53	43 47 50 52	connima	$⊢ (G \in TopGrp \land A \in X) \to J ↾_{𝑡} (z \in X ⟼ A +_{G} z) [S] \in Conn$
54	42 53	eqeltrd	$⊢ (G \in TopGrp \land A \in X) \to J ↾_{𝑡} [A] \underset{˙}{\sim} \in Conn$
55		eqid	$⊢ ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
56	55	conncompss	$⊢ ([A] \underset{˙}{\sim} \subseteq X \land A \in [A] \underset{˙}{\sim} \land J ↾_{𝑡} [A] \underset{˙}{\sim} \in Conn) \to [A] \underset{˙}{\sim} \subseteq ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
57	20 38 54 56	syl3anc	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} \subseteq ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
58		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
59	44	mptpreima	$⊢ {(z \in X ⟼ A +_{G} z)}^{-1} [y] = \{z \in X \| A +_{G} z \in y\}$
60	59	ssrab3	$⊢ {(z \in X ⟼ A +_{G} z)}^{-1} [y] \subseteq X$
61	29	adantr	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to \underset{˙}{0} \in X$
62	1 14 2	grprid	$⊢ (G \in Grp \land A \in X) \to A +_{G} \underset{˙}{0} = A$
63	22 62	sylan	$⊢ (G \in TopGrp \land A \in X) \to A +_{G} \underset{˙}{0} = A$
64	63	adantr	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to A +_{G} \underset{˙}{0} = A$
65		simprrl	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to A \in y$
66	64 65	eqeltrd	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to A +_{G} \underset{˙}{0} \in y$
67		oveq2	$⊢ z = \underset{˙}{0} \to A +_{G} z = A +_{G} \underset{˙}{0}$
68	67	eleq1d	$⊢ z = \underset{˙}{0} \to (A +_{G} z \in y \leftrightarrow A +_{G} \underset{˙}{0} \in y)$
69	68 59	elrab2	$⊢ \underset{˙}{0} \in {(z \in X ⟼ A +_{G} z)}^{-1} [y] \leftrightarrow (\underset{˙}{0} \in X \land A +_{G} \underset{˙}{0} \in y)$
70	61 66 69	sylanbrc	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to \underset{˙}{0} \in {(z \in X ⟼ A +_{G} z)}^{-1} [y]$
71		hmeocnvcn	$⊢ (z \in X ⟼ A +_{G} z) \in (J Homeo J) \to {(z \in X ⟼ A +_{G} z)}^{-1} \in (J Cn J)$
72	45 71	syl	$⊢ (G \in TopGrp \land A \in X) \to {(z \in X ⟼ A +_{G} z)}^{-1} \in (J Cn J)$
73	72	adantr	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to {(z \in X ⟼ A +_{G} z)}^{-1} \in (J Cn J)$
74		simprl	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to y \subseteq X$
75	49	adantr	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to X = ⋃ J$
76	74 75	sseqtrd	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to y \subseteq ⋃ J$
77		simprrr	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to J ↾_{𝑡} y \in Conn$
78	43 73 76 77	connima	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to J ↾_{𝑡} {(z \in X ⟼ A +_{G} z)}^{-1} [y] \in Conn$
79	4	conncompss	$⊢ ({(z \in X ⟼ A +_{G} z)}^{-1} [y] \subseteq X \land \underset{˙}{0} \in {(z \in X ⟼ A +_{G} z)}^{-1} [y] \land J ↾_{𝑡} {(z \in X ⟼ A +_{G} z)}^{-1} [y] \in Conn) \to {(z \in X ⟼ A +_{G} z)}^{-1} [y] \subseteq S$
80	60 70 78 79	mp3an2i	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to {(z \in X ⟼ A +_{G} z)}^{-1} [y] \subseteq S$
81		eqid	$⊢ (g \in X ⟼ (z \in X ⟼ g +_{G} z)) = (g \in X ⟼ (z \in X ⟼ g +_{G} z))$
82	81 1 14 13	grplactcnv	$⊢ (G \in Grp \land A \in X) \to ((g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A) : X \underset{1-1 onto}{⟶} X \land {(g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A)}^{-1} = (g \in X ⟼ (z \in X ⟼ g +_{G} z)) ({inv}_{g} (G) (A)))$
83	22 82	sylan	$⊢ (G \in TopGrp \land A \in X) \to ((g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A) : X \underset{1-1 onto}{⟶} X \land {(g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A)}^{-1} = (g \in X ⟼ (z \in X ⟼ g +_{G} z)) ({inv}_{g} (G) (A)))$
84	83	simpld	$⊢ (G \in TopGrp \land A \in X) \to (g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A) : X \underset{1-1 onto}{⟶} X$
85	81 1	grplactfval	$⊢ A \in X \to (g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A) = (z \in X ⟼ A +_{G} z)$
86	85	adantl	$⊢ (G \in TopGrp \land A \in X) \to (g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A) = (z \in X ⟼ A +_{G} z)$
87	86	f1oeq1d	$⊢ (G \in TopGrp \land A \in X) \to ((g \in X ⟼ (z \in X ⟼ g +_{G} z)) (A) : X \underset{1-1 onto}{⟶} X \leftrightarrow (z \in X ⟼ A +_{G} z) : X \underset{1-1 onto}{⟶} X)$
88	84 87	mpbid	$⊢ (G \in TopGrp \land A \in X) \to (z \in X ⟼ A +_{G} z) : X \underset{1-1 onto}{⟶} X$
89	88	adantr	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to (z \in X ⟼ A +_{G} z) : X \underset{1-1 onto}{⟶} X$
90		f1ocnv	$⊢ (z \in X ⟼ A +_{G} z) : X \underset{1-1 onto}{⟶} X \to {(z \in X ⟼ A +_{G} z)}^{-1} : X \underset{1-1 onto}{⟶} X$
91		f1ofun	$⊢ {(z \in X ⟼ A +_{G} z)}^{-1} : X \underset{1-1 onto}{⟶} X \to Fun {(z \in X ⟼ A +_{G} z)}^{-1}$
92	89 90 91	3syl	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to Fun {(z \in X ⟼ A +_{G} z)}^{-1}$
93		f1odm	$⊢ {(z \in X ⟼ A +_{G} z)}^{-1} : X \underset{1-1 onto}{⟶} X \to dom {(z \in X ⟼ A +_{G} z)}^{-1} = X$
94	89 90 93	3syl	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to dom {(z \in X ⟼ A +_{G} z)}^{-1} = X$
95	74 94	sseqtrrd	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to y \subseteq dom {(z \in X ⟼ A +_{G} z)}^{-1}$
96		funimass3	$⊢ (Fun {(z \in X ⟼ A +_{G} z)}^{-1} \land y \subseteq dom {(z \in X ⟼ A +_{G} z)}^{-1}) \to ({(z \in X ⟼ A +_{G} z)}^{-1} [y] \subseteq S \leftrightarrow y \subseteq {(z \in X ⟼ A +_{G} z)}^{-1}^{-1} [S])$
97	92 95 96	syl2anc	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to ({(z \in X ⟼ A +_{G} z)}^{-1} [y] \subseteq S \leftrightarrow y \subseteq {(z \in X ⟼ A +_{G} z)}^{-1}^{-1} [S])$
98	80 97	mpbid	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to y \subseteq {(z \in X ⟼ A +_{G} z)}^{-1}^{-1} [S]$
99	41	adantr	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to [A] \underset{˙}{\sim} = (z \in X ⟼ A +_{G} z) [S]$
100		imacnvcnv	$⊢ {(z \in X ⟼ A +_{G} z)}^{-1}^{-1} [S] = (z \in X ⟼ A +_{G} z) [S]$
101	99 100	eqtr4di	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to [A] \underset{˙}{\sim} = {(z \in X ⟼ A +_{G} z)}^{-1}^{-1} [S]$
102	98 101	sseqtrrd	$⊢ ((G \in TopGrp \land A \in X) \land (y \subseteq X \land (A \in y \land J ↾_{𝑡} y \in Conn))) \to y \subseteq [A] \underset{˙}{\sim}$
103	102	expr	$⊢ ((G \in TopGrp \land A \in X) \land y \subseteq X) \to ((A \in y \land J ↾_{𝑡} y \in Conn) \to y \subseteq [A] \underset{˙}{\sim})$
104	58 103	sylan2	$⊢ ((G \in TopGrp \land A \in X) \land y \in 𝒫 X) \to ((A \in y \land J ↾_{𝑡} y \in Conn) \to y \subseteq [A] \underset{˙}{\sim})$
105	104	ralrimiva	$⊢ (G \in TopGrp \land A \in X) \to \forall y \in 𝒫 X ((A \in y \land J ↾_{𝑡} y \in Conn) \to y \subseteq [A] \underset{˙}{\sim})$
106		eleq2w	$⊢ x = y \to (A \in x \leftrightarrow A \in y)$
107		oveq2	$⊢ x = y \to J ↾_{𝑡} x = J ↾_{𝑡} y$
108	107	eleq1d	$⊢ x = y \to (J ↾_{𝑡} x \in Conn \leftrightarrow J ↾_{𝑡} y \in Conn)$
109	106 108	anbi12d	$⊢ x = y \to ((A \in x \land J ↾_{𝑡} x \in Conn) \leftrightarrow (A \in y \land J ↾_{𝑡} y \in Conn))$
110	109	ralrab	$⊢ \forall y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} y \subseteq [A] \underset{˙}{\sim} \leftrightarrow \forall y \in 𝒫 X ((A \in y \land J ↾_{𝑡} y \in Conn) \to y \subseteq [A] \underset{˙}{\sim})$
111	105 110	sylibr	$⊢ (G \in TopGrp \land A \in X) \to \forall y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} y \subseteq [A] \underset{˙}{\sim}$
112		unissb	$⊢ ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq [A] \underset{˙}{\sim} \leftrightarrow \forall y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} y \subseteq [A] \underset{˙}{\sim}$
113	111 112	sylibr	$⊢ (G \in TopGrp \land A \in X) \to ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq [A] \underset{˙}{\sim}$
114	57 113	eqssd	$⊢ (G \in TopGrp \land A \in X) \to [A] \underset{˙}{\sim} = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$

Metamath Proof Explorer

Theorem tgpconncompeqg

Proof