Metamath Proof Explorer


Theorem symgtgp

Description: The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015) (Proof shortened by AV, 30-Mar-2024)

Ref Expression
Hypothesis symgtgp.g G=SymGrpA
Assertion symgtgp AVGTopGrp

Proof

Step Hyp Ref Expression
1 symgtgp.g G=SymGrpA
2 1 symggrp AVGGrp
3 eqid Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` A ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) with typecode |-
4 3 efmndtmd Could not format ( A e. V -> ( EndoFMnd ` A ) e. TopMnd ) : No typesetting found for |- ( A e. V -> ( EndoFMnd ` A ) e. TopMnd ) with typecode |-
5 eqid BaseG=BaseG
6 3 1 5 symgsubmefmnd Could not format ( A e. V -> ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) ) : No typesetting found for |- ( A e. V -> ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) ) with typecode |-
7 1 5 3 symgressbas Could not format G = ( ( EndoFMnd ` A ) |`s ( Base ` G ) ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s ( Base ` G ) ) with typecode |-
8 7 submtmd Could not format ( ( ( EndoFMnd ` A ) e. TopMnd /\ ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) ) -> G e. TopMnd ) : No typesetting found for |- ( ( ( EndoFMnd ` A ) e. TopMnd /\ ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) ) -> G e. TopMnd ) with typecode |-
9 4 6 8 syl2anc AVGTopMnd
10 eqid 𝑡A×𝒫A=𝑡A×𝒫A
11 1 5 symgtopn AV𝑡A×𝒫A𝑡BaseG=TopOpenG
12 distopon AV𝒫ATopOnA
13 10 pttoponconst AV𝒫ATopOnA𝑡A×𝒫ATopOnAA
14 12 13 mpdan AV𝑡A×𝒫ATopOnAA
15 1 5 elsymgbas AVxBaseGx:A1-1 ontoA
16 f1of x:A1-1 ontoAx:AA
17 elmapg AVAVxAAx:AA
18 17 anidms AVxAAx:AA
19 16 18 syl5ibr AVx:A1-1 ontoAxAA
20 15 19 sylbid AVxBaseGxAA
21 20 ssrdv AVBaseGAA
22 resttopon 𝑡A×𝒫ATopOnAABaseGAA𝑡A×𝒫A𝑡BaseGTopOnBaseG
23 14 21 22 syl2anc AV𝑡A×𝒫A𝑡BaseGTopOnBaseG
24 11 23 eqeltrrd AVTopOpenGTopOnBaseG
25 id AVAV
26 distop AV𝒫ATop
27 fconst6g 𝒫ATopA×𝒫A:ATop
28 26 27 syl AVA×𝒫A:ATop
29 15 biimpa AVxBaseGx:A1-1 ontoA
30 f1ocnv x:A1-1 ontoAx-1:A1-1 ontoA
31 f1of x-1:A1-1 ontoAx-1:AA
32 29 30 31 3syl AVxBaseGx-1:AA
33 32 ffvelrnda AVxBaseGyAx-1yA
34 33 an32s AVyAxBaseGx-1yA
35 34 fmpttd AVyAxBaseGx-1y:BaseGA
36 35 adantr AVyAfBaseGxBaseGx-1y:BaseGA
37 cnveq x=fx-1=f-1
38 37 fveq1d x=fx-1y=f-1y
39 eqid xBaseGx-1y=xBaseGx-1y
40 fvex f-1yV
41 38 39 40 fvmpt fBaseGxBaseGx-1yf=f-1y
42 41 ad2antlr AVyAfBaseGt𝒫AxBaseGx-1yf=f-1y
43 42 eleq1d AVyAfBaseGt𝒫AxBaseGx-1yftf-1yt
44 eqid uBaseGuf-1y=uBaseGuf-1y
45 44 mptiniseg yVuBaseGuf-1y-1y=uBaseG|uf-1y=y
46 45 elv uBaseGuf-1y-1y=uBaseG|uf-1y=y
47 eqid 𝑡A×𝒫A𝑡BaseG=𝑡A×𝒫A𝑡BaseG
48 14 ad2antrr AVyAfBaseG𝑡A×𝒫ATopOnAA
49 21 ad2antrr AVyAfBaseGBaseGAA
50 toponuni 𝑡A×𝒫ATopOnAAAA=𝑡A×𝒫A
51 mpteq1 AA=𝑡A×𝒫AuAAuf-1y=u𝑡A×𝒫Auf-1y
52 48 50 51 3syl AVyAfBaseGuAAuf-1y=u𝑡A×𝒫Auf-1y
53 simpll AVyAfBaseGAV
54 28 ad2antrr AVyAfBaseGA×𝒫A:ATop
55 1 5 elsymgbas AVfBaseGf:A1-1 ontoA
56 55 adantr AVyAfBaseGf:A1-1 ontoA
57 56 biimpa AVyAfBaseGf:A1-1 ontoA
58 f1ocnv f:A1-1 ontoAf-1:A1-1 ontoA
59 f1of f-1:A1-1 ontoAf-1:AA
60 57 58 59 3syl AVyAfBaseGf-1:AA
61 simplr AVyAfBaseGyA
62 60 61 ffvelrnd AVyAfBaseGf-1yA
63 eqid 𝑡A×𝒫A=𝑡A×𝒫A
64 63 10 ptpjcn AVA×𝒫A:ATopf-1yAu𝑡A×𝒫Auf-1y𝑡A×𝒫ACnA×𝒫Af-1y
65 53 54 62 64 syl3anc AVyAfBaseGu𝑡A×𝒫Auf-1y𝑡A×𝒫ACnA×𝒫Af-1y
66 26 ad2antrr AVyAfBaseG𝒫ATop
67 fvconst2g 𝒫ATopf-1yAA×𝒫Af-1y=𝒫A
68 66 62 67 syl2anc AVyAfBaseGA×𝒫Af-1y=𝒫A
69 68 oveq2d AVyAfBaseG𝑡A×𝒫ACnA×𝒫Af-1y=𝑡A×𝒫ACn𝒫A
70 65 69 eleqtrd AVyAfBaseGu𝑡A×𝒫Auf-1y𝑡A×𝒫ACn𝒫A
71 52 70 eqeltrd AVyAfBaseGuAAuf-1y𝑡A×𝒫ACn𝒫A
72 47 48 49 71 cnmpt1res AVyAfBaseGuBaseGuf-1y𝑡A×𝒫A𝑡BaseGCn𝒫A
73 11 oveq1d AV𝑡A×𝒫A𝑡BaseGCn𝒫A=TopOpenGCn𝒫A
74 73 ad2antrr AVyAfBaseG𝑡A×𝒫A𝑡BaseGCn𝒫A=TopOpenGCn𝒫A
75 72 74 eleqtrd AVyAfBaseGuBaseGuf-1yTopOpenGCn𝒫A
76 snelpwi yAy𝒫A
77 76 ad2antlr AVyAfBaseGy𝒫A
78 cnima uBaseGuf-1yTopOpenGCn𝒫Ay𝒫AuBaseGuf-1y-1yTopOpenG
79 75 77 78 syl2anc AVyAfBaseGuBaseGuf-1y-1yTopOpenG
80 46 79 eqeltrrid AVyAfBaseGuBaseG|uf-1y=yTopOpenG
81 80 adantr AVyAfBaseGt𝒫Af-1ytuBaseG|uf-1y=yTopOpenG
82 fveq1 u=fuf-1y=ff-1y
83 82 eqeq1d u=fuf-1y=yff-1y=y
84 simplr AVyAfBaseGt𝒫Af-1ytfBaseG
85 57 adantr AVyAfBaseGt𝒫Af-1ytf:A1-1 ontoA
86 simpllr AVyAfBaseGt𝒫Af-1ytyA
87 f1ocnvfv2 f:A1-1 ontoAyAff-1y=y
88 85 86 87 syl2anc AVyAfBaseGt𝒫Af-1ytff-1y=y
89 83 84 88 elrabd AVyAfBaseGt𝒫Af-1ytfuBaseG|uf-1y=y
90 ssrab2 uBaseG|uf-1y=yBaseG
91 90 a1i AVyAfBaseGt𝒫Af-1ytuBaseG|uf-1y=yBaseG
92 15 ad3antrrr AVyAfBaseGt𝒫Af-1ytxBaseGx:A1-1 ontoA
93 92 biimpa AVyAfBaseGt𝒫Af-1ytxBaseGx:A1-1 ontoA
94 62 ad2antrr AVyAfBaseGt𝒫Af-1ytxBaseGf-1yA
95 f1ocnvfv x:A1-1 ontoAf-1yAxf-1y=yx-1y=f-1y
96 93 94 95 syl2anc AVyAfBaseGt𝒫Af-1ytxBaseGxf-1y=yx-1y=f-1y
97 simplrr AVyAfBaseGt𝒫Af-1ytxBaseGf-1yt
98 eleq1 x-1y=f-1yx-1ytf-1yt
99 97 98 syl5ibrcom AVyAfBaseGt𝒫Af-1ytxBaseGx-1y=f-1yx-1yt
100 96 99 syld AVyAfBaseGt𝒫Af-1ytxBaseGxf-1y=yx-1yt
101 100 ralrimiva AVyAfBaseGt𝒫Af-1ytxBaseGxf-1y=yx-1yt
102 fveq1 u=xuf-1y=xf-1y
103 102 eqeq1d u=xuf-1y=yxf-1y=y
104 103 ralrab xuBaseG|uf-1y=yx-1ytxBaseGxf-1y=yx-1yt
105 101 104 sylibr AVyAfBaseGt𝒫Af-1ytxuBaseG|uf-1y=yx-1yt
106 ssrab uBaseG|uf-1y=yxBaseG|x-1ytuBaseG|uf-1y=yBaseGxuBaseG|uf-1y=yx-1yt
107 91 105 106 sylanbrc AVyAfBaseGt𝒫Af-1ytuBaseG|uf-1y=yxBaseG|x-1yt
108 39 mptpreima xBaseGx-1y-1t=xBaseG|x-1yt
109 107 108 sseqtrrdi AVyAfBaseGt𝒫Af-1ytuBaseG|uf-1y=yxBaseGx-1y-1t
110 funmpt FunxBaseGx-1y
111 fvex x-1yV
112 111 39 dmmpti domxBaseGx-1y=BaseG
113 91 112 sseqtrrdi AVyAfBaseGt𝒫Af-1ytuBaseG|uf-1y=ydomxBaseGx-1y
114 funimass3 FunxBaseGx-1yuBaseG|uf-1y=ydomxBaseGx-1yxBaseGx-1yuBaseG|uf-1y=ytuBaseG|uf-1y=yxBaseGx-1y-1t
115 110 113 114 sylancr AVyAfBaseGt𝒫Af-1ytxBaseGx-1yuBaseG|uf-1y=ytuBaseG|uf-1y=yxBaseGx-1y-1t
116 109 115 mpbird AVyAfBaseGt𝒫Af-1ytxBaseGx-1yuBaseG|uf-1y=yt
117 eleq2 v=uBaseG|uf-1y=yfvfuBaseG|uf-1y=y
118 imaeq2 v=uBaseG|uf-1y=yxBaseGx-1yv=xBaseGx-1yuBaseG|uf-1y=y
119 118 sseq1d v=uBaseG|uf-1y=yxBaseGx-1yvtxBaseGx-1yuBaseG|uf-1y=yt
120 117 119 anbi12d v=uBaseG|uf-1y=yfvxBaseGx-1yvtfuBaseG|uf-1y=yxBaseGx-1yuBaseG|uf-1y=yt
121 120 rspcev uBaseG|uf-1y=yTopOpenGfuBaseG|uf-1y=yxBaseGx-1yuBaseG|uf-1y=ytvTopOpenGfvxBaseGx-1yvt
122 81 89 116 121 syl12anc AVyAfBaseGt𝒫Af-1ytvTopOpenGfvxBaseGx-1yvt
123 122 expr AVyAfBaseGt𝒫Af-1ytvTopOpenGfvxBaseGx-1yvt
124 43 123 sylbid AVyAfBaseGt𝒫AxBaseGx-1yftvTopOpenGfvxBaseGx-1yvt
125 124 ralrimiva AVyAfBaseGt𝒫AxBaseGx-1yftvTopOpenGfvxBaseGx-1yvt
126 24 ad2antrr AVyAfBaseGTopOpenGTopOnBaseG
127 12 ad2antrr AVyAfBaseG𝒫ATopOnA
128 simpr AVyAfBaseGfBaseG
129 iscnp TopOpenGTopOnBaseG𝒫ATopOnAfBaseGxBaseGx-1yTopOpenGCnP𝒫AfxBaseGx-1y:BaseGAt𝒫AxBaseGx-1yftvTopOpenGfvxBaseGx-1yvt
130 126 127 128 129 syl3anc AVyAfBaseGxBaseGx-1yTopOpenGCnP𝒫AfxBaseGx-1y:BaseGAt𝒫AxBaseGx-1yftvTopOpenGfvxBaseGx-1yvt
131 36 125 130 mpbir2and AVyAfBaseGxBaseGx-1yTopOpenGCnP𝒫Af
132 131 ralrimiva AVyAfBaseGxBaseGx-1yTopOpenGCnP𝒫Af
133 cncnp TopOpenGTopOnBaseG𝒫ATopOnAxBaseGx-1yTopOpenGCn𝒫AxBaseGx-1y:BaseGAfBaseGxBaseGx-1yTopOpenGCnP𝒫Af
134 24 12 133 syl2anc AVxBaseGx-1yTopOpenGCn𝒫AxBaseGx-1y:BaseGAfBaseGxBaseGx-1yTopOpenGCnP𝒫Af
135 134 adantr AVyAxBaseGx-1yTopOpenGCn𝒫AxBaseGx-1y:BaseGAfBaseGxBaseGx-1yTopOpenGCnP𝒫Af
136 35 132 135 mpbir2and AVyAxBaseGx-1yTopOpenGCn𝒫A
137 fvconst2g 𝒫ATopyAA×𝒫Ay=𝒫A
138 26 137 sylan AVyAA×𝒫Ay=𝒫A
139 138 oveq2d AVyATopOpenGCnA×𝒫Ay=TopOpenGCn𝒫A
140 136 139 eleqtrrd AVyAxBaseGx-1yTopOpenGCnA×𝒫Ay
141 10 24 25 28 140 ptcn AVxBaseGyAx-1yTopOpenGCn𝑡A×𝒫A
142 eqid invgG=invgG
143 5 142 grpinvf GGrpinvgG:BaseGBaseG
144 2 143 syl AVinvgG:BaseGBaseG
145 144 feqmptd AVinvgG=xBaseGinvgGx
146 1 5 142 symginv xBaseGinvgGx=x-1
147 146 adantl AVxBaseGinvgGx=x-1
148 32 feqmptd AVxBaseGx-1=yAx-1y
149 147 148 eqtrd AVxBaseGinvgGx=yAx-1y
150 149 mpteq2dva AVxBaseGinvgGx=xBaseGyAx-1y
151 145 150 eqtrd AVinvgG=xBaseGyAx-1y
152 xkopt 𝒫ATopAV𝒫A^ko𝒫A=𝑡A×𝒫A
153 26 152 mpancom AV𝒫A^ko𝒫A=𝑡A×𝒫A
154 153 oveq2d AVTopOpenGCn𝒫A^ko𝒫A=TopOpenGCn𝑡A×𝒫A
155 141 151 154 3eltr4d AVinvgGTopOpenGCn𝒫A^ko𝒫A
156 eqid 𝒫A^ko𝒫A=𝒫A^ko𝒫A
157 156 xkotopon 𝒫ATop𝒫ATop𝒫A^ko𝒫ATopOn𝒫ACn𝒫A
158 26 26 157 syl2anc AV𝒫A^ko𝒫ATopOn𝒫ACn𝒫A
159 frn invgG:BaseGBaseGraninvgGBaseG
160 2 143 159 3syl AVraninvgGBaseG
161 cndis AV𝒫ATopOnA𝒫ACn𝒫A=AA
162 12 161 mpdan AV𝒫ACn𝒫A=AA
163 21 162 sseqtrrd AVBaseG𝒫ACn𝒫A
164 cnrest2 𝒫A^ko𝒫ATopOn𝒫ACn𝒫AraninvgGBaseGBaseG𝒫ACn𝒫AinvgGTopOpenGCn𝒫A^ko𝒫AinvgGTopOpenGCn𝒫A^ko𝒫A𝑡BaseG
165 158 160 163 164 syl3anc AVinvgGTopOpenGCn𝒫A^ko𝒫AinvgGTopOpenGCn𝒫A^ko𝒫A𝑡BaseG
166 155 165 mpbid AVinvgGTopOpenGCn𝒫A^ko𝒫A𝑡BaseG
167 153 oveq1d AV𝒫A^ko𝒫A𝑡BaseG=𝑡A×𝒫A𝑡BaseG
168 167 11 eqtrd AV𝒫A^ko𝒫A𝑡BaseG=TopOpenG
169 168 oveq2d AVTopOpenGCn𝒫A^ko𝒫A𝑡BaseG=TopOpenGCnTopOpenG
170 166 169 eleqtrd AVinvgGTopOpenGCnTopOpenG
171 eqid TopOpenG=TopOpenG
172 171 142 istgp GTopGrpGGrpGTopMndinvgGTopOpenGCnTopOpenG
173 2 9 170 172 syl3anbrc AVGTopGrp