Metamath Proof Explorer


Theorem qustgpopn

Description: A quotient map in a topological group is an open map. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qustgp.h H=G/𝑠G~QGY
qustgpopn.x X=BaseG
qustgpopn.j J=TopOpenG
qustgpopn.k K=TopOpenH
qustgpopn.f F=xXxG~QGY
Assertion qustgpopn GTopGrpYNrmSGrpGSJFSK

Proof

Step Hyp Ref Expression
1 qustgp.h H=G/𝑠G~QGY
2 qustgpopn.x X=BaseG
3 qustgpopn.j J=TopOpenG
4 qustgpopn.k K=TopOpenH
5 qustgpopn.f F=xXxG~QGY
6 imassrn FSranF
7 1 a1i GTopGrpYNrmSGrpGSJH=G/𝑠G~QGY
8 2 a1i GTopGrpYNrmSGrpGSJX=BaseG
9 ovex G~QGYV
10 9 a1i GTopGrpYNrmSGrpGSJG~QGYV
11 simp1 GTopGrpYNrmSGrpGSJGTopGrp
12 7 8 5 10 11 quslem GTopGrpYNrmSGrpGSJF:XontoX/G~QGY
13 forn F:XontoX/G~QGYranF=X/G~QGY
14 12 13 syl GTopGrpYNrmSGrpGSJranF=X/G~QGY
15 6 14 sseqtrid GTopGrpYNrmSGrpGSJFSX/G~QGY
16 eceq1 x=yxG~QGY=yG~QGY
17 16 cbvmptv xXxG~QGY=yXyG~QGY
18 5 17 eqtri F=yXyG~QGY
19 18 mptpreima F-1FS=yX|yG~QGYFS
20 19 rabeq2i yF-1FSyXyG~QGYFS
21 5 funmpt2 FunF
22 fvelima FunFyG~QGYFSzSFz=yG~QGY
23 21 22 mpan yG~QGYFSzSFz=yG~QGY
24 3 2 tgptopon GTopGrpJTopOnX
25 11 24 syl GTopGrpYNrmSGrpGSJJTopOnX
26 simp3 GTopGrpYNrmSGrpGSJSJ
27 toponss JTopOnXSJSX
28 25 26 27 syl2anc GTopGrpYNrmSGrpGSJSX
29 28 adantr GTopGrpYNrmSGrpGSJyXSX
30 29 sselda GTopGrpYNrmSGrpGSJyXzSzX
31 eceq1 x=zxG~QGY=zG~QGY
32 ecexg G~QGYVzG~QGYV
33 9 32 ax-mp zG~QGYV
34 31 5 33 fvmpt zXFz=zG~QGY
35 30 34 syl GTopGrpYNrmSGrpGSJyXzSFz=zG~QGY
36 35 eqeq1d GTopGrpYNrmSGrpGSJyXzSFz=yG~QGYzG~QGY=yG~QGY
37 eqcom zG~QGY=yG~QGYyG~QGY=zG~QGY
38 36 37 bitrdi GTopGrpYNrmSGrpGSJyXzSFz=yG~QGYyG~QGY=zG~QGY
39 nsgsubg YNrmSGrpGYSubGrpG
40 39 3ad2ant2 GTopGrpYNrmSGrpGSJYSubGrpG
41 40 ad2antrr GTopGrpYNrmSGrpGSJyXzSYSubGrpG
42 eqid G~QGY=G~QGY
43 2 42 eqger YSubGrpGG~QGYErX
44 41 43 syl GTopGrpYNrmSGrpGSJyXzSG~QGYErX
45 simplr GTopGrpYNrmSGrpGSJyXzSyX
46 44 45 erth GTopGrpYNrmSGrpGSJyXzSyG~QGYzyG~QGY=zG~QGY
47 11 ad2antrr GTopGrpYNrmSGrpGSJyXzSGTopGrp
48 2 subgss YSubGrpGYX
49 41 48 syl GTopGrpYNrmSGrpGSJyXzSYX
50 eqid invgG=invgG
51 eqid +G=+G
52 2 50 51 42 eqgval GTopGrpYXyG~QGYzyXzXinvgGy+GzY
53 47 49 52 syl2anc GTopGrpYNrmSGrpGSJyXzSyG~QGYzyXzXinvgGy+GzY
54 38 46 53 3bitr2d GTopGrpYNrmSGrpGSJyXzSFz=yG~QGYyXzXinvgGy+GzY
55 eqid opp𝑔G=opp𝑔G
56 eqid +opp𝑔G=+opp𝑔G
57 51 55 56 oppgplus invgGy+Gz+opp𝑔Ga=a+GinvgGy+Gz
58 57 mpteq2i aXinvgGy+Gz+opp𝑔Ga=aXa+GinvgGy+Gz
59 47 adantr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYGTopGrp
60 55 oppgtgp GTopGrpopp𝑔GTopGrp
61 59 60 syl GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYopp𝑔GTopGrp
62 49 sselda GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYinvgGy+GzX
63 eqid aXinvgGy+Gz+opp𝑔Ga=aXinvgGy+Gz+opp𝑔Ga
64 55 2 oppgbas X=Baseopp𝑔G
65 55 3 oppgtopn J=TopOpenopp𝑔G
66 63 64 56 65 tgplacthmeo opp𝑔GTopGrpinvgGy+GzXaXinvgGy+Gz+opp𝑔GaJHomeoJ
67 61 62 66 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGy+Gz+opp𝑔GaJHomeoJ
68 58 67 eqeltrrid GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXa+GinvgGy+GzJHomeoJ
69 hmeocn aXa+GinvgGy+GzJHomeoJaXa+GinvgGy+GzJCnJ
70 68 69 syl GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXa+GinvgGy+GzJCnJ
71 26 ad3antrrr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYSJ
72 cnima aXa+GinvgGy+GzJCnJSJaXa+GinvgGy+Gz-1SJ
73 70 71 72 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXa+GinvgGy+Gz-1SJ
74 45 adantr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYyX
75 tgpgrp GTopGrpGGrp
76 59 75 syl GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYGGrp
77 eqid 0G=0G
78 2 51 77 50 grprinv GGrpyXy+GinvgGy=0G
79 76 74 78 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYy+GinvgGy=0G
80 79 oveq1d GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYy+GinvgGy+Gz=0G+Gz
81 2 50 grpinvcl GGrpyXinvgGyX
82 76 74 81 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYinvgGyX
83 30 adantr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYzX
84 2 51 grpass GGrpyXinvgGyXzXy+GinvgGy+Gz=y+GinvgGy+Gz
85 76 74 82 83 84 syl13anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYy+GinvgGy+Gz=y+GinvgGy+Gz
86 2 51 77 grplid GGrpzX0G+Gz=z
87 76 83 86 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzY0G+Gz=z
88 80 85 87 3eqtr3d GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYy+GinvgGy+Gz=z
89 simplr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYzS
90 88 89 eqeltrd GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYy+GinvgGy+GzS
91 oveq1 a=ya+GinvgGy+Gz=y+GinvgGy+Gz
92 91 eleq1d a=ya+GinvgGy+GzSy+GinvgGy+GzS
93 eqid aXa+GinvgGy+Gz=aXa+GinvgGy+Gz
94 93 mptpreima aXa+GinvgGy+Gz-1S=aX|a+GinvgGy+GzS
95 92 94 elrab2 yaXa+GinvgGy+Gz-1SyXy+GinvgGy+GzS
96 74 90 95 sylanbrc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYyaXa+GinvgGy+Gz-1S
97 ecexg G~QGYVxG~QGYV
98 9 97 ax-mp xG~QGYV
99 98 5 fnmpti FFnX
100 29 ad3antrrr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXSX
101 fnfvima FFnXSXa+GinvgGy+GzSFa+GinvgGy+GzFS
102 101 3expia FFnXSXa+GinvgGy+GzSFa+GinvgGy+GzFS
103 99 100 102 sylancr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXa+GinvgGy+GzSFa+GinvgGy+GzFS
104 76 adantr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXGGrp
105 simpr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXaX
106 62 adantr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGy+GzX
107 2 51 grpcl GGrpaXinvgGy+GzXa+GinvgGy+GzX
108 104 105 106 107 syl3anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXa+GinvgGy+GzX
109 eceq1 x=a+GinvgGy+GzxG~QGY=a+GinvgGy+GzG~QGY
110 109 5 98 fvmpt3i a+GinvgGy+GzXFa+GinvgGy+Gz=a+GinvgGy+GzG~QGY
111 108 110 syl GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXFa+GinvgGy+Gz=a+GinvgGy+GzG~QGY
112 44 ad2antrr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXG~QGYErX
113 2 51 77 50 grplinv GGrpaXinvgGa+Ga=0G
114 104 105 113 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGa+Ga=0G
115 114 oveq1d GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGa+Ga+GinvgGy+Gz=0G+GinvgGy+Gz
116 2 50 grpinvcl GGrpaXinvgGaX
117 104 105 116 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGaX
118 2 51 grpass GGrpinvgGaXaXinvgGy+GzXinvgGa+Ga+GinvgGy+Gz=invgGa+Ga+GinvgGy+Gz
119 104 117 105 106 118 syl13anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGa+Ga+GinvgGy+Gz=invgGa+Ga+GinvgGy+Gz
120 2 51 77 grplid GGrpinvgGy+GzX0G+GinvgGy+Gz=invgGy+Gz
121 104 106 120 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaX0G+GinvgGy+Gz=invgGy+Gz
122 115 119 121 3eqtr3d GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGa+Ga+GinvgGy+Gz=invgGy+Gz
123 simplr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGy+GzY
124 122 123 eqeltrd GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXinvgGa+Ga+GinvgGy+GzY
125 49 ad2antrr GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXYX
126 2 50 51 42 eqgval GGrpYXaG~QGYa+GinvgGy+GzaXa+GinvgGy+GzXinvgGa+Ga+GinvgGy+GzY
127 104 125 126 syl2anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXaG~QGYa+GinvgGy+GzaXa+GinvgGy+GzXinvgGa+Ga+GinvgGy+GzY
128 105 108 124 127 mpbir3and GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXaG~QGYa+GinvgGy+Gz
129 112 128 erthi GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXaG~QGY=a+GinvgGy+GzG~QGY
130 111 129 eqtr4d GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXFa+GinvgGy+Gz=aG~QGY
131 130 eleq1d GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXFa+GinvgGy+GzFSaG~QGYFS
132 103 131 sylibd GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXa+GinvgGy+GzSaG~QGYFS
133 132 ss2rabdv GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaX|a+GinvgGy+GzSaX|aG~QGYFS
134 eceq1 x=axG~QGY=aG~QGY
135 134 cbvmptv xXxG~QGY=aXaG~QGY
136 5 135 eqtri F=aXaG~QGY
137 136 mptpreima F-1FS=aX|aG~QGYFS
138 133 94 137 3sstr4g GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYaXa+GinvgGy+Gz-1SF-1FS
139 eleq2 u=aXa+GinvgGy+Gz-1SyuyaXa+GinvgGy+Gz-1S
140 sseq1 u=aXa+GinvgGy+Gz-1SuF-1FSaXa+GinvgGy+Gz-1SF-1FS
141 139 140 anbi12d u=aXa+GinvgGy+Gz-1SyuuF-1FSyaXa+GinvgGy+Gz-1SaXa+GinvgGy+Gz-1SF-1FS
142 141 rspcev aXa+GinvgGy+Gz-1SJyaXa+GinvgGy+Gz-1SaXa+GinvgGy+Gz-1SF-1FSuJyuuF-1FS
143 73 96 138 142 syl12anc GTopGrpYNrmSGrpGSJyXzSinvgGy+GzYuJyuuF-1FS
144 143 3ad2antr3 GTopGrpYNrmSGrpGSJyXzSyXzXinvgGy+GzYuJyuuF-1FS
145 144 ex GTopGrpYNrmSGrpGSJyXzSyXzXinvgGy+GzYuJyuuF-1FS
146 54 145 sylbid GTopGrpYNrmSGrpGSJyXzSFz=yG~QGYuJyuuF-1FS
147 146 rexlimdva GTopGrpYNrmSGrpGSJyXzSFz=yG~QGYuJyuuF-1FS
148 23 147 syl5 GTopGrpYNrmSGrpGSJyXyG~QGYFSuJyuuF-1FS
149 148 expimpd GTopGrpYNrmSGrpGSJyXyG~QGYFSuJyuuF-1FS
150 20 149 syl5bi GTopGrpYNrmSGrpGSJyF-1FSuJyuuF-1FS
151 150 ralrimiv GTopGrpYNrmSGrpGSJyF-1FSuJyuuF-1FS
152 topontop JTopOnXJTop
153 eltop2 JTopF-1FSJyF-1FSuJyuuF-1FS
154 25 152 153 3syl GTopGrpYNrmSGrpGSJF-1FSJyF-1FSuJyuuF-1FS
155 151 154 mpbird GTopGrpYNrmSGrpGSJF-1FSJ
156 elqtop3 JTopOnXF:XontoX/G~QGYFSJqTopFFSX/G~QGYF-1FSJ
157 25 12 156 syl2anc GTopGrpYNrmSGrpGSJFSJqTopFFSX/G~QGYF-1FSJ
158 15 155 157 mpbir2and GTopGrpYNrmSGrpGSJFSJqTopF
159 7 8 5 10 11 qusval GTopGrpYNrmSGrpGSJH=F𝑠G
160 159 8 12 11 3 4 imastopn GTopGrpYNrmSGrpGSJK=JqTopF
161 158 160 eleqtrrd GTopGrpYNrmSGrpGSJFSK