Metamath Proof Explorer


Theorem pcoass

Description: Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Mario Carneiro, 8-Jun-2014)

Ref Expression
Hypotheses pcoass.2 φFIICnJ
pcoass.3 φGIICnJ
pcoass.4 φHIICnJ
pcoass.5 φF1=G0
pcoass.6 φG1=H0
pcoass.7 P=x01ifx12ifx142xx+14x2+12
Assertion pcoass φF*𝑝JG*𝑝JHphJF*𝑝JG*𝑝JH

Proof

Step Hyp Ref Expression
1 pcoass.2 φFIICnJ
2 pcoass.3 φGIICnJ
3 pcoass.4 φHIICnJ
4 pcoass.5 φF1=G0
5 pcoass.6 φG1=H0
6 pcoass.7 P=x01ifx12ifx142xx+14x2+12
7 iftrue x14ifx142xx+14=2x
8 7 fveq2d x14F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG*𝑝JH2x
9 8 adantl φx01x14F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG*𝑝JH2x
10 2cn 2
11 elicc01 x01x0xx1
12 11 simp1bi x01x
13 12 adantr x01x14x
14 13 recnd x01x14x
15 mulcom 2x2x=x2
16 10 14 15 sylancr x01x142x=x2
17 11 simp2bi x010x
18 17 adantr x01x140x
19 simpr x01x14x14
20 0re 0
21 4nn 4
22 nnrecre 414
23 21 22 ax-mp 14
24 20 23 elicc2i x014x0xx14
25 13 18 19 24 syl3anbrc x01x14x014
26 2rp 2+
27 10 mul02i 02=0
28 23 recni 14
29 28 2timesi 214=14+14
30 2ne0 20
31 recdiv2 220220122=122
32 10 30 10 30 31 mp4an 122=122
33 2t2e4 22=4
34 33 oveq2i 122=14
35 32 34 eqtri 122=14
36 35 35 oveq12i 122+122=14+14
37 halfcn 12
38 2halves 12122+122=12
39 37 38 ax-mp 122+122=12
40 36 39 eqtr3i 14+14=12
41 29 40 eqtri 214=12
42 10 28 41 mulcomli 142=12
43 20 23 26 27 42 iccdili x014x2012
44 25 43 syl x01x14x2012
45 16 44 eqeltrd x01x142x012
46 2 3 5 pcocn φG*𝑝JHIICnJ
47 1 46 pcoval1 φ2x012F*𝑝JG*𝑝JH2x=F22x
48 1 2 pcoval1 φ2x012F*𝑝JG2x=F22x
49 47 48 eqtr4d φ2x012F*𝑝JG*𝑝JH2x=F*𝑝JG2x
50 45 49 sylan2 φx01x14F*𝑝JG*𝑝JH2x=F*𝑝JG2x
51 50 anassrs φx01x14F*𝑝JG*𝑝JH2x=F*𝑝JG2x
52 9 51 eqtrd φx01x14F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG2x
53 52 adantlr φx01x12x14F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG2x
54 simplll φx01x12¬x14φ
55 12 ad2antlr φx01x12x
56 55 adantr φx01x12¬x14x
57 letric x14x1414x
58 55 23 57 sylancl φx01x12x1414x
59 58 orcanai φx01x12¬x1414x
60 simplr φx01x12¬x14x12
61 halfre 12
62 23 61 elicc2i x1412x14xx12
63 56 59 60 62 syl3anbrc φx01x12¬x14x1412
64 62 simp1bi x1412x
65 readdcl x14x+14
66 64 23 65 sylancl x1412x+14
67 23 a1i x141214
68 62 simp2bi x141214x
69 67 64 67 68 leadd1dd x141214+14x+14
70 40 69 eqbrtrrid x141212x+14
71 61 a1i x141212
72 62 simp3bi x1412x12
73 2lt4 2<4
74 2re 2
75 4re 4
76 2pos 0<2
77 4pos 0<4
78 74 75 76 77 ltrecii 2<414<12
79 73 78 mpbi 14<12
80 23 61 79 ltleii 1412
81 80 a1i x14121412
82 64 67 71 71 72 81 le2addd x1412x+1412+12
83 ax-1cn 1
84 2halves 112+12=1
85 83 84 ax-mp 12+12=1
86 82 85 breqtrdi x1412x+141
87 1re 1
88 61 87 elicc2i x+14121x+1412x+14x+141
89 66 70 86 88 syl3anbrc x1412x+14121
90 63 89 syl φx01x12¬x14x+14121
91 2 3 pco0 φG*𝑝JH0=G0
92 4 91 eqtr4d φF1=G*𝑝JH0
93 1 46 92 pcoval2 φx+14121F*𝑝JG*𝑝JHx+14=G*𝑝JH2x+141
94 54 90 93 syl2anc φx01x12¬x14F*𝑝JG*𝑝JHx+14=G*𝑝JH2x+141
95 85 oveq2i 2x+1412+12=2x+141
96 2cnd φx01x12¬x142
97 56 recnd φx01x12¬x14x
98 28 a1i φx01x12¬x1414
99 96 97 98 adddid φx01x12¬x142x+14=2x+214
100 41 oveq2i 2x+214=2x+12
101 99 100 eqtrdi φx01x12¬x142x+14=2x+12
102 101 oveq1d φx01x12¬x142x+1412+12=2x+12-12+12
103 95 102 eqtr3id φx01x12¬x142x+141=2x+12-12+12
104 remulcl 2x2x
105 74 56 104 sylancr φx01x12¬x142x
106 105 recnd φx01x12¬x142x
107 37 a1i φx01x12¬x1412
108 106 107 107 pnpcan2d φx01x12¬x142x+12-12+12=2x12
109 103 108 eqtrd φx01x12¬x142x+141=2x12
110 109 fveq2d φx01x12¬x14G*𝑝JH2x+141=G*𝑝JH2x12
111 10 97 15 sylancr φx01x12¬x142x=x2
112 83 10 30 divcan1i 122=1
113 23 61 26 42 112 iccdili x1412x2121
114 63 113 syl φx01x12¬x14x2121
115 111 114 eqeltrd φx01x12¬x142x121
116 37 subidi 1212=0
117 1mhlfehlf 112=12
118 61 87 61 116 117 iccshftli 2x1212x12012
119 115 118 syl φx01x12¬x142x12012
120 2 3 pcoval1 φ2x12012G*𝑝JH2x12=G22x12
121 54 119 120 syl2anc φx01x12¬x14G*𝑝JH2x12=G22x12
122 96 106 107 subdid φx01x12¬x1422x12=22x212
123 10 30 recidi 212=1
124 123 oveq2i 22x212=22x1
125 122 124 eqtrdi φx01x12¬x1422x12=22x1
126 125 fveq2d φx01x12¬x14G22x12=G22x1
127 121 126 eqtrd φx01x12¬x14G*𝑝JH2x12=G22x1
128 94 110 127 3eqtrd φx01x12¬x14F*𝑝JG*𝑝JHx+14=G22x1
129 iffalse ¬x14ifx142xx+14=x+14
130 129 fveq2d ¬x14F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG*𝑝JHx+14
131 130 adantl φx01x12¬x14F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG*𝑝JHx+14
132 1 2 4 pcoval2 φ2x121F*𝑝JG2x=G22x1
133 54 115 132 syl2anc φx01x12¬x14F*𝑝JG2x=G22x1
134 128 131 133 3eqtr4d φx01x12¬x14F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG2x
135 53 134 pm2.61dan φx01x12F*𝑝JG*𝑝JHifx142xx+14=F*𝑝JG2x
136 iftrue x12ifx12ifx142xx+14x2+12=ifx142xx+14
137 136 fveq2d x12F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=F*𝑝JG*𝑝JHifx142xx+14
138 137 adantl φx01x12F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=F*𝑝JG*𝑝JHifx142xx+14
139 iftrue x12ifx12F*𝑝JG2xH2x1=F*𝑝JG2x
140 139 adantl φx01x12ifx12F*𝑝JG2xH2x1=F*𝑝JG2x
141 135 138 140 3eqtr4d φx01x12F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=ifx12F*𝑝JG2xH2x1
142 elii2 x01¬x12x121
143 halfge0 012
144 halflt1 12<1
145 61 87 144 ltleii 121
146 elicc01 120112012121
147 61 143 145 146 mpbir3an 1201
148 1elunit 101
149 iccss2 120110112101
150 147 148 149 mp2an 12101
151 150 sseli x121x01
152 10 30 div0i 02=0
153 eqid 12=12
154 20 87 26 152 153 icccntri x01x2012
155 37 addid2i 0+12=12
156 20 61 61 155 85 iccshftri x2012x2+12121
157 151 154 156 3syl x121x2+12121
158 1 46 92 pcoval2 φx2+12121F*𝑝JG*𝑝JHx2+12=G*𝑝JH2x2+121
159 157 158 sylan2 φx121F*𝑝JG*𝑝JHx2+12=G*𝑝JH2x2+121
160 61 87 elicc2i x121x12xx1
161 160 simp1bi x121x
162 161 recnd x121x
163 1cnd x1211
164 2cnd x1212
165 30 a1i x12120
166 162 163 164 165 divdird x121x+12=x2+12
167 166 oveq2d x1212x+12=2x2+12
168 peano2cn xx+1
169 162 168 syl x121x+1
170 169 164 165 divcan2d x1212x+12=x+1
171 167 170 eqtr3d x1212x2+12=x+1
172 162 163 171 mvrraddd x1212x2+121=x
173 172 fveq2d x121G*𝑝JH2x2+121=G*𝑝JHx
174 173 adantl φx121G*𝑝JH2x2+121=G*𝑝JHx
175 2 3 5 pcoval2 φx121G*𝑝JHx=H2x1
176 159 174 175 3eqtrd φx121F*𝑝JG*𝑝JHx2+12=H2x1
177 142 176 sylan2 φx01¬x12F*𝑝JG*𝑝JHx2+12=H2x1
178 177 anassrs φx01¬x12F*𝑝JG*𝑝JHx2+12=H2x1
179 iffalse ¬x12ifx12ifx142xx+14x2+12=x2+12
180 179 fveq2d ¬x12F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=F*𝑝JG*𝑝JHx2+12
181 180 adantl φx01¬x12F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=F*𝑝JG*𝑝JHx2+12
182 iffalse ¬x12ifx12F*𝑝JG2xH2x1=H2x1
183 182 adantl φx01¬x12ifx12F*𝑝JG2xH2x1=H2x1
184 178 181 183 3eqtr4d φx01¬x12F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=ifx12F*𝑝JG2xH2x1
185 141 184 pm2.61dan φx01F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=ifx12F*𝑝JG2xH2x1
186 185 mpteq2dva φx01F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12=x01ifx12F*𝑝JG2xH2x1
187 iitopon IITopOn01
188 187 a1i φIITopOn01
189 188 cnmptid φx01xIICnII
190 0elunit 001
191 190 a1i φ001
192 188 188 191 cnmptc φx010IICnII
193 eqid topGenran.=topGenran.
194 eqid topGenran.𝑡012=topGenran.𝑡012
195 eqid topGenran.𝑡121=topGenran.𝑡121
196 dfii2 II=topGenran.𝑡01
197 0red φ0
198 1red φ1
199 147 a1i φ1201
200 simprl φy=12z01y=12
201 200 oveq1d φy=12z01y+14=12+14
202 37 28 addcomi 12+14=14+12
203 201 202 eqtrdi φy=12z01y+14=14+12
204 23 61 ltnlei 14<12¬1214
205 79 204 mpbi ¬1214
206 200 breq1d φy=12z01y141214
207 205 206 mtbiri φy=12z01¬y14
208 207 iffalsed φy=12z01ify142yy+14=y+14
209 200 oveq1d φy=12z01y2=122
210 209 35 eqtrdi φy=12z01y2=14
211 210 oveq1d φy=12z01y2+12=14+12
212 203 208 211 3eqtr4d φy=12z01ify142yy+14=y2+12
213 eqid topGenran.𝑡014=topGenran.𝑡014
214 eqid topGenran.𝑡1412=topGenran.𝑡1412
215 61 a1i φ12
216 75 77 recgt0ii 0<14
217 20 23 216 ltleii 014
218 20 61 elicc2i 14012140141412
219 23 217 80 218 mpbir3an 14012
220 219 a1i φ14012
221 simprl φy=14z01y=14
222 221 oveq2d φy=14z012y=214
223 221 oveq1d φy=14z01y+14=14+14
224 29 222 223 3eqtr4a φy=14z012y=y+14
225 retopon topGenran.TopOn
226 0xr 0*
227 61 rexri 12*
228 lbicc2 0*12*0120012
229 226 227 143 228 mp3an 0012
230 iccss2 001214012014012
231 229 219 230 mp2an 014012
232 iccssre 012012
233 20 61 232 mp2an 012
234 231 233 sstri 014
235 resttopon topGenran.TopOn014topGenran.𝑡014TopOn014
236 225 234 235 mp2an topGenran.𝑡014TopOn014
237 236 a1i φtopGenran.𝑡014TopOn014
238 237 188 cnmpt1st φy014,z01ytopGenran.𝑡014×tIICntopGenran.𝑡014
239 retop topGenran.Top
240 ovex 012V
241 restabs topGenran.Top014012012VtopGenran.𝑡012𝑡014=topGenran.𝑡014
242 239 231 240 241 mp3an topGenran.𝑡012𝑡014=topGenran.𝑡014
243 242 eqcomi topGenran.𝑡014=topGenran.𝑡012𝑡014
244 resttopon topGenran.TopOn012topGenran.𝑡012TopOn012
245 225 233 244 mp2an topGenran.𝑡012TopOn012
246 245 a1i φtopGenran.𝑡012TopOn012
247 231 a1i φ014012
248 194 iihalf1cn x0122xtopGenran.𝑡012CnII
249 248 a1i φx0122xtopGenran.𝑡012CnII
250 243 246 247 249 cnmpt1res φx0142xtopGenran.𝑡014CnII
251 oveq2 x=y2x=2y
252 237 188 238 237 250 251 cnmpt21 φy014,z012ytopGenran.𝑡014×tIICnII
253 iccssre 14121412
254 23 61 253 mp2an 1412
255 resttopon topGenran.TopOn1412topGenran.𝑡1412TopOn1412
256 225 254 255 mp2an topGenran.𝑡1412TopOn1412
257 256 a1i φtopGenran.𝑡1412TopOn1412
258 257 188 cnmpt1st φy1412,z01ytopGenran.𝑡1412×tIICntopGenran.𝑡1412
259 eqid TopOpenfld=TopOpenfld
260 254 a1i φ1412
261 unitssre 01
262 261 a1i φ01
263 150 89 sselid x1412x+1401
264 263 adantl φx1412x+1401
265 259 cnfldtopon TopOpenfldTopOn
266 265 a1i φTopOpenfldTopOn
267 266 cnmptid φxxTopOpenfldCnTopOpenfld
268 23 a1i φ14
269 268 recnd φ14
270 266 266 269 cnmptc φx14TopOpenfldCnTopOpenfld
271 259 addcn +TopOpenfld×tTopOpenfldCnTopOpenfld
272 271 a1i φ+TopOpenfld×tTopOpenfldCnTopOpenfld
273 266 267 270 272 cnmpt12f φxx+14TopOpenfldCnTopOpenfld
274 259 214 196 260 262 264 273 cnmptre φx1412x+14topGenran.𝑡1412CnII
275 oveq1 x=yx+14=y+14
276 257 188 258 257 274 275 cnmpt21 φy1412,z01y+14topGenran.𝑡1412×tIICnII
277 193 213 214 194 197 215 220 188 224 252 276 cnmpopc φy012,z01ify142yy+14topGenran.𝑡012×tIICnII
278 iccssre 121121
279 61 87 278 mp2an 121
280 resttopon topGenran.TopOn121topGenran.𝑡121TopOn121
281 225 279 280 mp2an topGenran.𝑡121TopOn121
282 281 a1i φtopGenran.𝑡121TopOn121
283 282 188 cnmpt1st φy121,z01ytopGenran.𝑡121×tIICntopGenran.𝑡121
284 279 a1i φ121
285 150 157 sselid x121x2+1201
286 285 adantl φx121x2+1201
287 259 divccn 220xx2TopOpenfldCnTopOpenfld
288 10 30 287 mp2an xx2TopOpenfldCnTopOpenfld
289 288 a1i φxx2TopOpenfldCnTopOpenfld
290 37 a1i φ12
291 266 266 290 cnmptc φx12TopOpenfldCnTopOpenfld
292 266 289 291 272 cnmpt12f φxx2+12TopOpenfldCnTopOpenfld
293 259 195 196 284 262 286 292 cnmptre φx121x2+12topGenran.𝑡121CnII
294 oveq1 x=yx2=y2
295 294 oveq1d x=yx2+12=y2+12
296 282 188 283 282 293 295 cnmpt21 φy121,z01y2+12topGenran.𝑡121×tIICnII
297 193 194 195 196 197 198 199 188 212 277 296 cnmpopc φy01,z01ify12ify142yy+14y2+12II×tIICnII
298 breq1 x=yx12y12
299 breq1 x=yx14y14
300 299 251 275 ifbieq12d x=yifx142xx+14=ify142yy+14
301 298 300 295 ifbieq12d x=yifx12ifx142xx+14x2+12=ify12ify142yy+14y2+12
302 301 equcoms y=xifx12ifx142xx+14x2+12=ify12ify142yy+14y2+12
303 302 adantr y=xz=0ifx12ifx142xx+14x2+12=ify12ify142yy+14y2+12
304 303 eqcomd y=xz=0ify12ify142yy+14y2+12=ifx12ifx142xx+14x2+12
305 188 189 192 188 188 297 304 cnmpt12 φx01ifx12ifx142xx+14x2+12IICnII
306 6 305 eqeltrid φPIICnII
307 iiuni 01=II
308 307 307 cnf PIICnIIP:0101
309 306 308 syl φP:0101
310 6 fmpt x01ifx12ifx142xx+14x2+1201P:0101
311 309 310 sylibr φx01ifx12ifx142xx+14x2+1201
312 6 a1i φP=x01ifx12ifx142xx+14x2+12
313 1 46 92 pcocn φF*𝑝JG*𝑝JHIICnJ
314 eqid J=J
315 307 314 cnf F*𝑝JG*𝑝JHIICnJF*𝑝JG*𝑝JH:01J
316 313 315 syl φF*𝑝JG*𝑝JH:01J
317 316 feqmptd φF*𝑝JG*𝑝JH=y01F*𝑝JG*𝑝JHy
318 fveq2 y=ifx12ifx142xx+14x2+12F*𝑝JG*𝑝JHy=F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12
319 311 312 317 318 fmptcof φF*𝑝JG*𝑝JHP=x01F*𝑝JG*𝑝JHifx12ifx142xx+14x2+12
320 1 2 4 pcocn φF*𝑝JGIICnJ
321 320 3 pcoval φF*𝑝JG*𝑝JH=x01ifx12F*𝑝JG2xH2x1
322 186 319 321 3eqtr4rd φF*𝑝JG*𝑝JH=F*𝑝JG*𝑝JHP
323 id x=0x=0
324 323 143 eqbrtrdi x=0x12
325 324 iftrued x=0ifx12ifx142xx+14x2+12=ifx142xx+14
326 323 217 eqbrtrdi x=0x14
327 326 iftrued x=0ifx142xx+14=2x
328 oveq2 x=02x=20
329 2t0e0 20=0
330 328 329 eqtrdi x=02x=0
331 325 327 330 3eqtrd x=0ifx12ifx142xx+14x2+12=0
332 c0ex 0V
333 331 6 332 fvmpt 001P0=0
334 191 333 syl φP0=0
335 148 a1i φ101
336 61 87 ltnlei 12<1¬112
337 144 336 mpbi ¬112
338 breq1 x=1x12112
339 337 338 mtbiri x=1¬x12
340 339 iffalsed x=1ifx12ifx142xx+14x2+12=x2+12
341 oveq1 x=1x2=12
342 341 oveq1d x=1x2+12=12+12
343 342 85 eqtrdi x=1x2+12=1
344 340 343 eqtrd x=1ifx12ifx142xx+14x2+12=1
345 1ex 1V
346 344 6 345 fvmpt 101P1=1
347 335 346 syl φP1=1
348 313 306 334 347 reparpht φF*𝑝JG*𝑝JHPphJF*𝑝JG*𝑝JH
349 322 348 eqbrtrd φF*𝑝JG*𝑝JHphJF*𝑝JG*𝑝JH