Theorem tgpconncompeqg 23935

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

Hypotheses

Ref	Expression
tgpconncomp.x	⊢ 𝑋 = (Base‘𝐺)
tgpconncomp.z	⊢ 0 = (0g‘𝐺)
tgpconncomp.j	⊢ 𝐽 = (TopOpen‘𝐺)
tgpconncomp.s	⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
tgpconncompeqg.r	⊢ ∼ = (𝐺 ~QG 𝑆)

Assertion

Ref	Expression
tgpconncompeqg	⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})

Distinct variable groups:   𝑥, 0   𝑥,𝐴   𝑥,𝐽   𝑥,𝐺   𝑥,𝑋

Allowed substitution hints:   ∼ (𝑥)   𝑆(𝑥)

Proof of Theorem tgpconncompeqg

Dummy variables 𝑦 𝑧 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfec2 8712	. . . . 5 ⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
2	1	adantl 481	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
3		tgpconncomp.s	. . . . . . . . 9 ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
4		ssrab2 4077	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋
5		sspwuni 5103	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋)
6	4, 5	mpbi 229	. . . . . . . . 9 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋
7	3, 6	eqsstri 4016	. . . . . . . 8 ⊢ 𝑆 ⊆ 𝑋
8	7	a1i 11	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ 𝑋)
9		tgpconncomp.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
10		eqid 2731	. . . . . . . 8 ⊢ (invg‘𝐺) = (invg‘𝐺)
11		eqid 2731	. . . . . . . 8 ⊢ (+g‘𝐺) = (+g‘𝐺)
12		tgpconncompeqg.r	. . . . . . . 8 ⊢ ∼ = (𝐺 ~QG 𝑆)
13	9, 10, 11, 12	eqgval 19100	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆)))
14	8, 13	syldan 590	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆)))
15		simp2 1136	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆) → 𝑧 ∈ 𝑋)
16	14, 15	syl6bi 253	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 → 𝑧 ∈ 𝑋))
17	16	abssdv 4065	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → {𝑧 ∣ 𝐴 ∼ 𝑧} ⊆ 𝑋)
18	2, 17	eqsstrd 4020	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ 𝑋)
19		simpr 484	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
20		tgpgrp 23901	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
21		tgpconncomp.z	. . . . . . . 8 ⊢ 0 = (0g‘𝐺)
22	9, 11, 21, 10	grplinv 18917	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
23	20, 22	sylan 579	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
24		tgpconncomp.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝐺)
25	24, 9	tgptopon 23905	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
26	25	adantr 480	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
27	20	adantr 480	. . . . . . . 8 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐺 ∈ Grp)
28	9, 21	grpidcl 18893	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋)
29	27, 28	syl 17	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑋)
30	3	conncompid 23254	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆)
31	26, 29, 30	syl2anc 583	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑆)
32	23, 31	eqeltrd 2832	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)
33	9, 10, 11, 12	eqgval 19100	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
34	8, 33	syldan 590	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
35	19, 19, 32, 34	mpbir3and 1341	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∼ 𝐴)
36		elecg 8752	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
37	19, 19, 36	syl2anc 583	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
38	35, 37	mpbird 257	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴] ∼ )
39	9, 12, 11	eqglact 19102	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
40	7, 39	mp3an2 1448	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
41	20, 40	sylan 579	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
42	41	oveq2d 7428	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) = (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
43		eqid 2731	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
44		eqid 2731	. . . . . . 7 ⊢ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))
45	44, 9, 11, 24	tgplacthmeo 23926	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
46		hmeocn 23583	. . . . . 6 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
47	45, 46	syl 17	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
48		toponuni 22735	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
49	26, 48	syl 17	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
50	7, 49	sseqtrid 4034	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ ∪ 𝐽)
51	3	conncompconn 23255	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
52	26, 29, 51	syl2anc 583	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
53	43, 47, 50, 52	connima 23248	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn)
54	42, 53	eqeltrd 2832	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) ∈ Conn)
55		eqid 2731	. . . 4 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
56	55	conncompss 23256	. . 3 ⊢ (([𝐴] ∼ ⊆ 𝑋 ∧ 𝐴 ∈ [𝐴] ∼ ∧ (𝐽 ↾t [𝐴] ∼ ) ∈ Conn) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
57	18, 38, 54, 56	syl3anc 1370	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
58		elpwi 4609	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋)
59	44	mptpreima 6237	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) = {𝑧 ∈ 𝑋 ∣ (𝐴(+g‘𝐺)𝑧) ∈ 𝑦}
60	59	ssrab3 4080	. . . . . . . . . 10 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋
61	29	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ 𝑋)
62	9, 11, 21	grprid 18896	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
63	20, 62	sylan 579	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
64	63	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
65		simprrl 778	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝐴 ∈ 𝑦)
66	64, 65	eqeltrd 2832	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐴(+g‘𝐺) 0 ) ∈ 𝑦)
67		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → (𝐴(+g‘𝐺)𝑧) = (𝐴(+g‘𝐺) 0 ))
68	67	eleq1d 2817	. . . . . . . . . . . 12 ⊢ (𝑧 = 0 → ((𝐴(+g‘𝐺)𝑧) ∈ 𝑦 ↔ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
69	68, 59	elrab2 3686	. . . . . . . . . . 11 ⊢ ( 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ↔ ( 0 ∈ 𝑋 ∧ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
70	61, 66, 69	sylanbrc 582	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦))
71		hmeocnvcn 23584	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
72	45, 71	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
73	72	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
74		simprl 768	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ 𝑋)
75	49	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑋 = ∪ 𝐽)
76	74, 75	sseqtrd 4022	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ ∪ 𝐽)
77		simprrr 779	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t 𝑦) ∈ Conn)
78	43, 73, 76, 77	connima 23248	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn)
79	3	conncompss 23256	. . . . . . . . . 10 ⊢ (((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋 ∧ 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ∧ (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
80	60, 70, 78, 79	mp3an2i 1465	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
81		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧))) = (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))
82	81, 9, 11, 10	grplactcnv 18969	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘((invg‘𝐺)‘𝐴))))
83	20, 82	sylan 579	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘((invg‘𝐺)‘𝐴))))
84	83	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋)
85	81, 9	grplactfval 18967	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
86	85	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
87	86	f1oeq1d 6828	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ↔ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋))
88	84, 87	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
89	88	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
90		f1ocnv 6845	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
91		f1ofun 6835	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
92	89, 90, 91	3syl 18	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
93		f1odm 6837	. . . . . . . . . . . 12 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
94	89, 90, 93	3syl 18	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
95	74, 94	sseqtrrd 4023	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
96		funimass3 7055	. . . . . . . . . 10 ⊢ ((Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∧ 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
97	92, 95, 96	syl2anc 583	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
98	80, 97	mpbid 231	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
99	41	adantr 480	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
100		imacnvcnv 6205	. . . . . . . . 9 ⊢ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆) = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)
101	99, 100	eqtr4di 2789	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → [𝐴] ∼ = (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
102	98, 101	sseqtrrd 4023	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ [𝐴] ∼ )
103	102	expr 456	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ⊆ 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
104	58, 103	sylan2 592	. . . . 5 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝒫 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
105	104	ralrimiva 3145	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
106		eleq2w 2816	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
107		oveq2 7420	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐽 ↾t 𝑥) = (𝐽 ↾t 𝑦))
108	107	eleq1d 2817	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝐽 ↾t 𝑥) ∈ Conn ↔ (𝐽 ↾t 𝑦) ∈ Conn))
109	106, 108	anbi12d 630	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn) ↔ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn)))
110	109	ralrab 3689	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
111	105, 110	sylibr 233	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
112		unissb 4943	. . 3 ⊢ (∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
113	111, 112	sylibr 233	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ )
114	57, 113	eqssd 3999	1 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  {cab 2708  ∀wral 3060  {crab 3431   ⊆ wss 3948  𝒫 cpw 4602  ∪ cuni 4908   class class class wbr 5148   ↦ cmpt 5231  ^◡ccnv 5675  dom cdm 5676   “ cima 5679  Fun wfun 6537  –1-1-onto→wf1o 6542  ‘cfv 6543  (class class class)co 7412  [cec 8707  Basecbs 17151  +_gcplusg 17204   ↾_t crest 17373  TopOpenctopn 17374  0_gc0g 17392  Grpcgrp 18861  inv_gcminusg 18862   ~_QG cqg 19045  TopOnctopon 22731   Cn ccn 23047  Conncconn 23234  Homeochmeo 23576  TopGrpctgp 23894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-ec 8711  df-map 8828  df-en 8946  df-fin 8949  df-fi 9412  df-rest 17375  df-0g 17394  df-topgen 17396  df-plusf 18570  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-grp 18864  df-minusg 18865  df-eqg 19048  df-top 22715  df-topon 22732  df-topsp 22754  df-bases 22768  df-cld 22842  df-cn 23050  df-cnp 23051  df-conn 23235  df-tx 23385  df-hmeo 23578  df-tmd 23895  df-tgp 23896

This theorem is referenced by:  tgpconncomp  23936