MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcorevlem Unicode version

Theorem pcorevlem 20698
Description: Lemma for pcorev 20699. Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)
Hypotheses
Ref Expression
pcorev.1
pcorev.2
pcorevlem.3
Assertion
Ref Expression
pcorevlem
Distinct variable groups:   , , ,   , ,   J, , ,   P, , ,

Proof of Theorem pcorevlem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pcorev.1 . . . . 5
2 iitopon 20555 . . . . . . 7
32a1i 11 . . . . . 6
4 iirevcn 20602 . . . . . . 7
54a1i 11 . . . . . 6
6 id 22 . . . . . 6
73, 5, 6cnmpt11f 19337 . . . . 5
81, 7syl5eqel 2540 . . . 4
9 1elunit 11489 . . . . 5
10 oveq2 6182 . . . . . . . 8
11 1m1e0 10475 . . . . . . . 8
1210, 11syl6eq 2506 . . . . . . 7
1312fveq2d 5777 . . . . . 6
14 fvex 5783 . . . . . 6
1513, 1, 14fvmpt 5857 . . . . 5
169, 15mp1i 12 . . . 4
178, 6, 16pcocn 20689 . . 3
18 cntop2 18945 . . . . . 6
19 eqid 2450 . . . . . . 7
2019toptopon 18638 . . . . . 6
2118, 20sylib 196 . . . . 5
22 iiuni 20557 . . . . . . 7
2322, 19cnf 18950 . . . . . 6
24 ffvelrn 5924 . . . . . 6
2523, 9, 24sylancl 662 . . . . 5
26 pcorev.2 . . . . . 6
2726pcoptcl 20693 . . . . 5
2821, 25, 27syl2anc 661 . . . 4
2928simp1d 1000 . . 3
30 pcorevlem.3 . . . 4
31 eqid 2450 . . . . . 6
32 eqid 2450 . . . . . 6
33 eqid 2450 . . . . . 6
34 dfii2 20558 . . . . . 6
35 0red 9472 . . . . . 6
36 1red 9486 . . . . . 6
37 halfre 10625 . . . . . . . 8
38 0re 9471 . . . . . . . . 9
39 halfgt0 10627 . . . . . . . . 9
4038, 37, 39ltleii 9582 . . . . . . . 8
41 1re 9470 . . . . . . . . 9
42 halflt1 10628 . . . . . . . . 9
4337, 41, 42ltleii 9582 . . . . . . . 8
4438, 41elicc2i 11446 . . . . . . . 8
4537, 40, 43, 44mpbir3an 1170 . . . . . . 7
4645a1i 11 . . . . . 6
47 simprl 755 . . . . . . . . . . 11
4847oveq2d 6190 . . . . . . . . . 10
49 2cn 10477 . . . . . . . . . . 11
50 2ne0 10499 . . . . . . . . . . 11
5149, 50recidi 10147 . . . . . . . . . 10
5248, 51syl6eq 2506 . . . . . . . . 9
5352oveq1d 6189 . . . . . . . . . . . 12
5453, 11syl6eq 2506 . . . . . . . . . . 11
5554oveq2d 6190 . . . . . . . . . 10
56 1m0e1 10517 . . . . . . . . . 10
5755, 56syl6eq 2506 . . . . . . . . 9
5852, 57eqtr4d 2493 . . . . . . . 8
5958oveq2d 6190 . . . . . . 7
6059oveq2d 6190 . . . . . 6
61 retopon 20442 . . . . . . . . 9
62 iccssre 11462 . . . . . . . . . 10
6338, 37, 62mp2an 672 . . . . . . . . 9
64 resttopon 18865 . . . . . . . . 9
6561, 63, 64mp2an 672 . . . . . . . 8
6665a1i 11 . . . . . . 7
6766, 3cnmpt2nd 19342 . . . . . . . . 9
68 oveq2 6182 . . . . . . . . 9
6966, 3, 67, 3, 5, 68cnmpt21 19344 . . . . . . . 8
7066, 3cnmpt1st 19341 . . . . . . . . 9
7132iihalf1cn 20604 . . . . . . . . . 10
7271a1i 11 . . . . . . . . 9
73 oveq2 6182 . . . . . . . . 9
7466, 3, 70, 66, 72, 73cnmpt21 19344 . . . . . . . 8
75 iimulcn 20610 . . . . . . . . 9
7675a1i 11 . . . . . . . 8
77 oveq12 6183 . . . . . . . 8
7866, 3, 69, 74, 3, 3, 76, 77cnmpt22 19347 . . . . . . 7
79 oveq2 6182 . . . . . . 7
8066, 3, 78, 3, 5, 79cnmpt21 19344 . . . . . 6
81 iccssre 11462 . . . . . . . . . 10
8237, 41, 81mp2an 672 . . . . . . . . 9
83 resttopon 18865 . . . . . . . . 9
8461, 82, 83mp2an 672 . . . . . . . 8
8584a1i 11 . . . . . . 7
8685, 3cnmpt2nd 19342 . . . . . . . . 9
8785, 3, 86, 3, 5, 68cnmpt21 19344 . . . . . . . 8
8885, 3cnmpt1st 19341 . . . . . . . . . 10
8933iihalf2cn 20606 . . . . . . . . . . 11
9089a1i 11 . . . . . . . . . 10
9173oveq1d 6189 . . . . . . . . . 10
9285, 3, 88, 85, 90, 91cnmpt21 19344 . . . . . . . . 9
93 oveq2 6182 . . . . . . . . 9
9485, 3, 92, 3, 5, 93cnmpt21 19344 . . . . . . . 8
95 oveq12 6183 . . . . . . . 8
9685, 3, 87, 94, 3, 3, 76, 95cnmpt22 19347 . . . . . . 7
97 oveq2 6182 . . . . . . 7
9885, 3, 96, 3, 5, 97cnmpt21 19344 . . . . . 6
9931, 32, 33, 34, 35, 36, 46, 3, 60, 80, 98cnmpt2pc 20600 . . . . 5
1003, 3, 99, 6cnmpt21f 19345 . . . 4
10130, 100syl5eqel 2540 . . 3
102 simpr 461 . . . . 5
103 0elunit 11488 . . . . 5
104 simpl 457 . . . . . . . . 9
105104breq1d 4384 . . . . . . . 8
106 simpr 461 . . . . . . . . . . . 12
107106oveq2d 6190 . . . . . . . . . . 11
108107, 56syl6eq 2506 . . . . . . . . . 10
109104oveq2d 6190 . . . . . . . . . 10
110108, 109oveq12d 6192 . . . . . . . . 9
111110oveq2d 6190 . . . . . . . 8
112109oveq1d 6189 . . . . . . . . . . 11
113112oveq2d 6190 . . . . . . . . . 10
114108, 113oveq12d 6192 . . . . . . . . 9
115114oveq2d 6190 . . . . . . . 8
116105, 111, 115ifbieq12d 3898 . . . . . . 7
117116fveq2d 5777 . . . . . 6
118 fvex 5783 . . . . . 6
119117, 30, 118ovmpt2a 6305 . . . . 5
120102, 103, 119sylancl 662 . . . 4
121 iftrue 3879 . . . . . . . 8
122121adantl 466 . . . . . . 7
123122fveq2d 5777 . . . . . 6
124 elii1 20607 . . . . . . . 8
1258, 6pcoval1 20685 . . . . . . . . 9
126 iihalf1 20603 . . . . . . . . . . 11
127126adantl 466 . . . . . . . . . 10
128 oveq2 6182 . . . . . . . . . . . . 13
129128fveq2d 5777 . . . . . . . . . . . 12
130 fvex 5783 . . . . . . . . . . . 12
131129, 1, 130fvmpt 5857 . . . . . . . . . . 11
132 unitssre 11517 . . . . . . . . . . . . . . . 16
133132sseli 3434 . . . . . . . . . . . . . . 15
134133recnd 9497 . . . . . . . . . . . . . 14
135134mulid2d 9489 . . . . . . . . . . . . 13
136135oveq2d 6190 . . . . . . . . . . . 12
137136fveq2d 5777 . . . . . . . . . . 11
138131, 137eqtr4d 2493 . . . . . . . . . 10
139127, 138syl 16 . . . . . . . . 9
140125, 139eqtrd 2490 . . . . . . . 8
141124, 140sylan2br 476 . . . . . . 7
142141anassrs 648 . . . . . 6
143123, 142eqtr4d 2493 . . . . 5
144 iffalse 3881 . . . . . . . 8
145144adantl 466 . . . . . . 7
146145fveq2d 5777 . . . . . 6
147 elii2 20608 . . . . . . . 8
1488, 6, 16pcoval2 20688 . . . . . . . . 9
149 iihalf2 20605 . . . . . . . . . . . 12
150149adantl 466 . . . . . . . . . . 11
151 ax-1cn 9425 . . . . . . . . . . . . . . 15
152132sseli 3434 . . . . . . . . . . . . . . . 16
153152recnd 9497 . . . . . . . . . . . . . . 15
154 subcl 9694 . . . . . . . . . . . . . . 15
155151, 153, 154sylancr 663 . . . . . . . . . . . . . 14
156155mulid2d 9489 . . . . . . . . . . . . 13
157156oveq2d 6190 . . . . . . . . . . . 12
158 nncan 9723 . . . . . . . . . . . . 13
159151, 153, 158sylancr 663 . . . . . . . . . . . 12
160157, 159eqtr2d 2491 . . . . . . . . . . 11
161150, 160syl 16 . . . . . . . . . 10
162161fveq2d 5777 . . . . . . . . 9
163148, 162eqtrd 2490 . . . . . . . 8
164147, 163sylan2 474 . . . . . . 7
165164anassrs 648 . . . . . 6
166146, 165eqtr4d 2493 . . . . 5
167143, 166pm2.61dan 789 . . . 4
168120, 167eqtrd 2490 . . 3
169132sseli 3434 . . . . . . . . . . . . 13
170169recnd 9497 . . . . . . . . . . . 12
171 mulcl 9451 . . . . . . . . . . . 12
17249, 170, 171sylancr 663 . . . . . . . . . . 11
173172adantl 466 . . . . . . . . . 10
174173mul02d 9652 . . . . . . . . 9
175174oveq2d 6190 . . . . . . . 8
176175, 56syl6eq 2506 . . . . . . 7
177 subcl 9694 . . . . . . . . . . . 12
178173, 151, 177sylancl 662 . . . . . . . . . . 11
179151, 178, 154sylancr 663 . . . . . . . . . 10
180179mul02d 9652 . . . . . . . . 9
181180oveq2d 6190 . . . . . . . 8
182181, 56syl6eq 2506 . . . . . . 7
183176, 182ifeq12d 3891 . . . . . 6
184 ifid 3908 . . . . . 6
185183, 184syl6eq 2506 . . . . 5
186185fveq2d 5777 . . . 4
187 simpl 457 . . . . . . . . 9
188187breq1d 4384 . . . . . . . 8
189 simpr 461 . . . . . . . . . . . 12
190189oveq2d 6190 . . . . . . . . . . 11
191190, 11syl6eq 2506 . . . . . . . . . 10
192187oveq2d 6190 . . . . . . . . . 10
193191, 192oveq12d 6192 . . . . . . . . 9
194193oveq2d 6190 . . . . . . . 8
195192oveq1d 6189 . . . . . . . . . . 11
196195oveq2d 6190 . . . . . . . . . 10
197191, 196oveq12d 6192 . . . . . . . . 9
198197oveq2d 6190 . . . . . . . 8
199188, 194, 198ifbieq12d 3898 . . . . . . 7
200199fveq2d 5777 . . . . . 6
201 fvex 5783 . . . . . 6
202200, 30, 201ovmpt2a 6305 . . . . 5
203102, 9, 202sylancl 662 . . . 4
20426fveq1i 5774 . . . . 5
205 fvex 5783 . . . . . . 7
206205fvconst2 6016 . . . . . 6
207206adantl 466 . . . . 5
208204, 207syl5eq 2502 . . . 4
209186, 203, 2083eqtr4d 2500 . . 3
210 simpl 457 . . . . . . . . . . 11
211210, 40syl6eqbr 4411 . . . . . . . . . 10
212 iftrue 3879 . . . . . . . . . 10
213211, 212syl 16 . . . . . . . . 9
214 simpr 461 . . . . . . . . . . . 12
215214oveq2d 6190 . . . . . . . . . . 11
216210oveq2d 6190 . . . . . . . . . . . 12
217 2t0e0 10562 . . . . . . . . . . . 12
218216, 217syl6eq 2506 . . . . . . . . . . 11
219215, 218oveq12d 6192 . . . . . . . . . 10
220219oveq2d 6190 . . . . . . . . 9
221213, 220eqtrd 2490 . . . . . . . 8