Metamath Proof Explorer


Theorem 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=BaseG
tgpconncomp.z 0˙=0G
tgpconncomp.j J=TopOpenG
tgpconncomp.s S=x𝒫X|0˙xJ𝑡xConn
tgpconncompeqg.r ˙=G~QGS
Assertion tgpconncompeqg GTopGrpAXA˙=x𝒫X|AxJ𝑡xConn

Proof

Step Hyp Ref Expression
1 tgpconncomp.x X=BaseG
2 tgpconncomp.z 0˙=0G
3 tgpconncomp.j J=TopOpenG
4 tgpconncomp.s S=x𝒫X|0˙xJ𝑡xConn
5 tgpconncompeqg.r ˙=G~QGS
6 dfec2 AXA˙=z|A˙z
7 6 adantl GTopGrpAXA˙=z|A˙z
8 ssrab2 x𝒫X|0˙xJ𝑡xConn𝒫X
9 sspwuni x𝒫X|0˙xJ𝑡xConn𝒫Xx𝒫X|0˙xJ𝑡xConnX
10 8 9 mpbi x𝒫X|0˙xJ𝑡xConnX
11 4 10 eqsstri SX
12 11 a1i GTopGrpAXSX
13 eqid invgG=invgG
14 eqid +G=+G
15 1 13 14 5 eqgval GTopGrpSXA˙zAXzXinvgGA+GzS
16 12 15 syldan GTopGrpAXA˙zAXzXinvgGA+GzS
17 simp2 AXzXinvgGA+GzSzX
18 16 17 syl6bi GTopGrpAXA˙zzX
19 18 abssdv GTopGrpAXz|A˙zX
20 7 19 eqsstrd GTopGrpAXA˙X
21 simpr GTopGrpAXAX
22 tgpgrp GTopGrpGGrp
23 1 14 2 13 grplinv GGrpAXinvgGA+GA=0˙
24 22 23 sylan GTopGrpAXinvgGA+GA=0˙
25 3 1 tgptopon GTopGrpJTopOnX
26 25 adantr GTopGrpAXJTopOnX
27 22 adantr GTopGrpAXGGrp
28 1 2 grpidcl GGrp0˙X
29 27 28 syl GTopGrpAX0˙X
30 4 conncompid JTopOnX0˙X0˙S
31 26 29 30 syl2anc GTopGrpAX0˙S
32 24 31 eqeltrd GTopGrpAXinvgGA+GAS
33 1 13 14 5 eqgval GTopGrpSXA˙AAXAXinvgGA+GAS
34 12 33 syldan GTopGrpAXA˙AAXAXinvgGA+GAS
35 21 21 32 34 mpbir3and GTopGrpAXA˙A
36 elecg AXAXAA˙A˙A
37 21 21 36 syl2anc GTopGrpAXAA˙A˙A
38 35 37 mpbird GTopGrpAXAA˙
39 1 5 14 eqglact GGrpSXAXA˙=zXA+GzS
40 11 39 mp3an2 GGrpAXA˙=zXA+GzS
41 22 40 sylan GTopGrpAXA˙=zXA+GzS
42 41 oveq2d GTopGrpAXJ𝑡A˙=J𝑡zXA+GzS
43 eqid J=J
44 eqid zXA+Gz=zXA+Gz
45 44 1 14 3 tgplacthmeo GTopGrpAXzXA+GzJHomeoJ
46 hmeocn zXA+GzJHomeoJzXA+GzJCnJ
47 45 46 syl GTopGrpAXzXA+GzJCnJ
48 toponuni JTopOnXX=J
49 26 48 syl GTopGrpAXX=J
50 11 49 sseqtrid GTopGrpAXSJ
51 4 conncompconn JTopOnX0˙XJ𝑡SConn
52 26 29 51 syl2anc GTopGrpAXJ𝑡SConn
53 43 47 50 52 connima GTopGrpAXJ𝑡zXA+GzSConn
54 42 53 eqeltrd GTopGrpAXJ𝑡A˙Conn
55 eqid x𝒫X|AxJ𝑡xConn=x𝒫X|AxJ𝑡xConn
56 55 conncompss A˙XAA˙J𝑡A˙ConnA˙x𝒫X|AxJ𝑡xConn
57 20 38 54 56 syl3anc GTopGrpAXA˙x𝒫X|AxJ𝑡xConn
58 elpwi y𝒫XyX
59 44 mptpreima zXA+Gz-1y=zX|A+Gzy
60 59 ssrab3 zXA+Gz-1yX
61 29 adantr GTopGrpAXyXAyJ𝑡yConn0˙X
62 1 14 2 grprid GGrpAXA+G0˙=A
63 22 62 sylan GTopGrpAXA+G0˙=A
64 63 adantr GTopGrpAXyXAyJ𝑡yConnA+G0˙=A
65 simprrl GTopGrpAXyXAyJ𝑡yConnAy
66 64 65 eqeltrd GTopGrpAXyXAyJ𝑡yConnA+G0˙y
67 oveq2 z=0˙A+Gz=A+G0˙
68 67 eleq1d z=0˙A+GzyA+G0˙y
69 68 59 elrab2 0˙zXA+Gz-1y0˙XA+G0˙y
70 61 66 69 sylanbrc GTopGrpAXyXAyJ𝑡yConn0˙zXA+Gz-1y
71 hmeocnvcn zXA+GzJHomeoJzXA+Gz-1JCnJ
72 45 71 syl GTopGrpAXzXA+Gz-1JCnJ
73 72 adantr GTopGrpAXyXAyJ𝑡yConnzXA+Gz-1JCnJ
74 simprl GTopGrpAXyXAyJ𝑡yConnyX
75 49 adantr GTopGrpAXyXAyJ𝑡yConnX=J
76 74 75 sseqtrd GTopGrpAXyXAyJ𝑡yConnyJ
77 simprrr GTopGrpAXyXAyJ𝑡yConnJ𝑡yConn
78 43 73 76 77 connima GTopGrpAXyXAyJ𝑡yConnJ𝑡zXA+Gz-1yConn
79 4 conncompss zXA+Gz-1yX0˙zXA+Gz-1yJ𝑡zXA+Gz-1yConnzXA+Gz-1yS
80 60 70 78 79 mp3an2i GTopGrpAXyXAyJ𝑡yConnzXA+Gz-1yS
81 eqid gXzXg+Gz=gXzXg+Gz
82 81 1 14 13 grplactcnv GGrpAXgXzXg+GzA:X1-1 ontoXgXzXg+GzA-1=gXzXg+GzinvgGA
83 22 82 sylan GTopGrpAXgXzXg+GzA:X1-1 ontoXgXzXg+GzA-1=gXzXg+GzinvgGA
84 83 simpld GTopGrpAXgXzXg+GzA:X1-1 ontoX
85 81 1 grplactfval AXgXzXg+GzA=zXA+Gz
86 85 adantl GTopGrpAXgXzXg+GzA=zXA+Gz
87 86 f1oeq1d GTopGrpAXgXzXg+GzA:X1-1 ontoXzXA+Gz:X1-1 ontoX
88 84 87 mpbid GTopGrpAXzXA+Gz:X1-1 ontoX
89 88 adantr GTopGrpAXyXAyJ𝑡yConnzXA+Gz:X1-1 ontoX
90 f1ocnv zXA+Gz:X1-1 ontoXzXA+Gz-1:X1-1 ontoX
91 f1ofun zXA+Gz-1:X1-1 ontoXFunzXA+Gz-1
92 89 90 91 3syl GTopGrpAXyXAyJ𝑡yConnFunzXA+Gz-1
93 f1odm zXA+Gz-1:X1-1 ontoXdomzXA+Gz-1=X
94 89 90 93 3syl GTopGrpAXyXAyJ𝑡yConndomzXA+Gz-1=X
95 74 94 sseqtrrd GTopGrpAXyXAyJ𝑡yConnydomzXA+Gz-1
96 funimass3 FunzXA+Gz-1ydomzXA+Gz-1zXA+Gz-1ySyzXA+Gz-1-1S
97 92 95 96 syl2anc GTopGrpAXyXAyJ𝑡yConnzXA+Gz-1ySyzXA+Gz-1-1S
98 80 97 mpbid GTopGrpAXyXAyJ𝑡yConnyzXA+Gz-1-1S
99 41 adantr GTopGrpAXyXAyJ𝑡yConnA˙=zXA+GzS
100 imacnvcnv zXA+Gz-1-1S=zXA+GzS
101 99 100 eqtr4di GTopGrpAXyXAyJ𝑡yConnA˙=zXA+Gz-1-1S
102 98 101 sseqtrrd GTopGrpAXyXAyJ𝑡yConnyA˙
103 102 expr GTopGrpAXyXAyJ𝑡yConnyA˙
104 58 103 sylan2 GTopGrpAXy𝒫XAyJ𝑡yConnyA˙
105 104 ralrimiva GTopGrpAXy𝒫XAyJ𝑡yConnyA˙
106 eleq2w x=yAxAy
107 oveq2 x=yJ𝑡x=J𝑡y
108 107 eleq1d x=yJ𝑡xConnJ𝑡yConn
109 106 108 anbi12d x=yAxJ𝑡xConnAyJ𝑡yConn
110 109 ralrab yx𝒫X|AxJ𝑡xConnyA˙y𝒫XAyJ𝑡yConnyA˙
111 105 110 sylibr GTopGrpAXyx𝒫X|AxJ𝑡xConnyA˙
112 unissb x𝒫X|AxJ𝑡xConnA˙yx𝒫X|AxJ𝑡xConnyA˙
113 111 112 sylibr GTopGrpAXx𝒫X|AxJ𝑡xConnA˙
114 57 113 eqssd GTopGrpAXA˙=x𝒫X|AxJ𝑡xConn