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

Theorem pcorevlem 20298
Description: Lemma for pcorev 20299. 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 20155 . . . . . . 7
32a1i 11 . . . . . 6
4 iirevcn 20202 . . . . . . 7
54a1i 11 . . . . . 6
6 id 21 . . . . . 6
73, 5, 6cnmpt11f 18941 . . . . 5
81, 7syl5eqel 2506 . . . 4
9 1elunit 11348 . . . . 5
10 oveq2 6069 . . . . . . . 8
11 1m1e0 10336 . . . . . . . 8
1210, 11syl6eq 2470 . . . . . . 7
1312fveq2d 5665 . . . . . 6
14 fvex 5671 . . . . . 6
1513, 1, 14fvmpt 5744 . . . . 5
169, 15mp1i 12 . . . 4
178, 6, 16pcocn 20289 . . 3
18 cntop2 18549 . . . . . 6
19 eqid 2422 . . . . . . 7
2019toptopon 18242 . . . . . 6
2118, 20sylib 190 . . . . 5
22 iiuni 20157 . . . . . . 7
2322, 19cnf 18554 . . . . . 6
24 ffvelrn 5811 . . . . . 6
2523, 9, 24sylancl 647 . . . . 5
26 pcorev.2 . . . . . 6
2726pcoptcl 20293 . . . . 5
2821, 25, 27syl2anc 646 . . . 4
2928simp1d 985 . . 3
30 pcorevlem.3 . . . 4
31 eqid 2422 . . . . . 6
32 eqid 2422 . . . . . 6
33 eqid 2422 . . . . . 6
34 dfii2 20158 . . . . . 6
35 0red 9333 . . . . . 6
36 1red 9347 . . . . . 6
37 halfre 10486 . . . . . . . 8
38 0re 9332 . . . . . . . . 9
39 halfgt0 10488 . . . . . . . . 9
4038, 37, 39ltleii 9443 . . . . . . . 8
41 1re 9331 . . . . . . . . 9
42 halflt1 10489 . . . . . . . . 9
4337, 41, 42ltleii 9443 . . . . . . . 8
4438, 41elicc2i 11306 . . . . . . . 8
4537, 40, 43, 44mpbir3an 1155 . . . . . . 7
4645a1i 11 . . . . . 6
47 simprl 740 . . . . . . . . . . 11
4847oveq2d 6077 . . . . . . . . . 10
49 2cn 10338 . . . . . . . . . . 11
50 2ne0 10360 . . . . . . . . . . 11
5149, 50recidi 10008 . . . . . . . . . 10
5248, 51syl6eq 2470 . . . . . . . . 9
5352oveq1d 6076 . . . . . . . . . . . 12
5453, 11syl6eq 2470 . . . . . . . . . . 11
5554oveq2d 6077 . . . . . . . . . 10
56 1m0e1 10378 . . . . . . . . . 10
5755, 56syl6eq 2470 . . . . . . . . 9
5852, 57eqtr4d 2457 . . . . . . . 8
5958oveq2d 6077 . . . . . . 7
6059oveq2d 6077 . . . . . 6
61 retopon 20042 . . . . . . . . 9
62 iccssre 11322 . . . . . . . . . 10
6338, 37, 62mp2an 657 . . . . . . . . 9
64 resttopon 18469 . . . . . . . . 9
6561, 63, 64mp2an 657 . . . . . . . 8
6665a1i 11 . . . . . . 7
6766, 3cnmpt2nd 18946 . . . . . . . . 9
68 oveq2 6069 . . . . . . . . 9
6966, 3, 67, 3, 5, 68cnmpt21 18948 . . . . . . . 8
7066, 3cnmpt1st 18945 . . . . . . . . 9
7132iihalf1cn 20204 . . . . . . . . . 10
7271a1i 11 . . . . . . . . 9
73 oveq2 6069 . . . . . . . . 9
7466, 3, 70, 66, 72, 73cnmpt21 18948 . . . . . . . 8
75 iimulcn 20210 . . . . . . . . 9
7675a1i 11 . . . . . . . 8
77 oveq12 6070 . . . . . . . 8
7866, 3, 69, 74, 3, 3, 76, 77cnmpt22 18951 . . . . . . 7
79 oveq2 6069 . . . . . . 7
8066, 3, 78, 3, 5, 79cnmpt21 18948 . . . . . 6
81 iccssre 11322 . . . . . . . . . 10
8237, 41, 81mp2an 657 . . . . . . . . 9
83 resttopon 18469 . . . . . . . . 9
8461, 82, 83mp2an 657 . . . . . . . 8
8584a1i 11 . . . . . . 7
8685, 3cnmpt2nd 18946 . . . . . . . . 9
8785, 3, 86, 3, 5, 68cnmpt21 18948 . . . . . . . 8
8885, 3cnmpt1st 18945 . . . . . . . . . 10
8933iihalf2cn 20206 . . . . . . . . . . 11
9089a1i 11 . . . . . . . . . 10
9173oveq1d 6076 . . . . . . . . . 10
9285, 3, 88, 85, 90, 91cnmpt21 18948 . . . . . . . . 9
93 oveq2 6069 . . . . . . . . 9
9485, 3, 92, 3, 5, 93cnmpt21 18948 . . . . . . . 8
95 oveq12 6070 . . . . . . . 8
9685, 3, 87, 94, 3, 3, 76, 95cnmpt22 18951 . . . . . . 7
97 oveq2 6069 . . . . . . 7
9885, 3, 96, 3, 5, 97cnmpt21 18948 . . . . . 6
9931, 32, 33, 34, 35, 36, 46, 3, 60, 80, 98cnmpt2pc 20200 . . . . 5
1003, 3, 99, 6cnmpt21f 18949 . . . 4
10130, 100syl5eqel 2506 . . 3
102 simpr 451 . . . . 5
103 0elunit 11347 . . . . 5
104 simpl 447 . . . . . . . . 9
105104breq1d 4277 . . . . . . . 8
106 simpr 451 . . . . . . . . . . . 12
107106oveq2d 6077 . . . . . . . . . . 11
108107, 56syl6eq 2470 . . . . . . . . . 10
109104oveq2d 6077 . . . . . . . . . 10
110108, 109oveq12d 6079 . . . . . . . . 9
111110oveq2d 6077 . . . . . . . 8
112109oveq1d 6076 . . . . . . . . . . 11
113112oveq2d 6077 . . . . . . . . . 10
114108, 113oveq12d 6079 . . . . . . . . 9
115114oveq2d 6077 . . . . . . . 8
116105, 111, 115ifbieq12d 3793 . . . . . . 7
117116fveq2d 5665 . . . . . 6
118 fvex 5671 . . . . . 6
119117, 30, 118ovmpt2a 6191 . . . . 5
120102, 103, 119sylancl 647 . . . 4
121 iftrue 3774 . . . . . . . 8
122121adantl 456 . . . . . . 7
123122fveq2d 5665 . . . . . 6
124 elii1 20207 . . . . . . . 8
1258, 6pcoval1 20285 . . . . . . . . 9
126 iihalf1 20203 . . . . . . . . . . 11
127126adantl 456 . . . . . . . . . 10
128 oveq2 6069 . . . . . . . . . . . . 13
129128fveq2d 5665 . . . . . . . . . . . 12
130 fvex 5671 . . . . . . . . . . . 12
131129, 1, 130fvmpt 5744 . . . . . . . . . . 11
132 unitssre 11376 . . . . . . . . . . . . . . . 16
133132sseli 3329 . . . . . . . . . . . . . . 15
134133recnd 9358 . . . . . . . . . . . . . 14
135134mulid2d 9350 . . . . . . . . . . . . 13
136135oveq2d 6077 . . . . . . . . . . . 12
137136fveq2d 5665 . . . . . . . . . . 11
138131, 137eqtr4d 2457 . . . . . . . . . 10
139127, 138syl 16 . . . . . . . . 9
140125, 139eqtrd 2454 . . . . . . . 8
141124, 140sylan2br 466 . . . . . . 7
142141anassrs 633 . . . . . 6
143123, 142eqtr4d 2457 . . . . 5
144 iffalse 3776 . . . . . . . 8
145144adantl 456 . . . . . . 7
146145fveq2d 5665 . . . . . 6
147 elii2 20208 . . . . . . . 8
1488, 6, 16pcoval2 20288 . . . . . . . . 9
149 iihalf2 20205 . . . . . . . . . . . 12
150149adantl 456 . . . . . . . . . . 11
151 ax-1cn 9286 . . . . . . . . . . . . . . 15
152132sseli 3329 . . . . . . . . . . . . . . . 16
153152recnd 9358 . . . . . . . . . . . . . . 15
154 subcl 9555 . . . . . . . . . . . . . . 15
155151, 153, 154sylancr 648 . . . . . . . . . . . . . 14
156155mulid2d 9350 . . . . . . . . . . . . 13
157156oveq2d 6077 . . . . . . . . . . . 12
158 nncan 9584 . . . . . . . . . . . . 13
159151, 153, 158sylancr 648 . . . . . . . . . . . 12
160157, 159eqtr2d 2455 . . . . . . . . . . 11
161150, 160syl 16 . . . . . . . . . 10
162161fveq2d 5665 . . . . . . . . 9
163148, 162eqtrd 2454 . . . . . . . 8
164147, 163sylan2 464 . . . . . . 7
165164anassrs 633 . . . . . 6
166146, 165eqtr4d 2457 . . . . 5
167143, 166pm2.61dan 774 . . . 4
168120, 167eqtrd 2454 . . 3
169132sseli 3329 . . . . . . . . . . . . 13
170169recnd 9358 . . . . . . . . . . . 12
171 mulcl 9312 . . . . . . . . . . . 12
17249, 170, 171sylancr 648 . . . . . . . . . . 11
173172adantl 456 . . . . . . . . . 10
174173mul02d 9513 . . . . . . . . 9
175174oveq2d 6077 . . . . . . . 8
176175, 56syl6eq 2470 . . . . . . 7
177 subcl 9555 . . . . . . . . . . . 12
178173, 151, 177sylancl 647 . . . . . . . . . . 11
179151, 178, 154sylancr 648 . . . . . . . . . 10
180179mul02d 9513 . . . . . . . . 9
181180oveq2d 6077 . . . . . . . 8
182181, 56syl6eq 2470 . . . . . . 7
183176, 182ifeq12d 3786 . . . . . 6
184 ifid 3803 . . . . . 6
185183, 184syl6eq 2470 . . . . 5
186185fveq2d 5665 . . . 4
187 simpl 447 . . . . . . . . 9
188187breq1d 4277 . . . . . . . 8
189 simpr 451 . . . . . . . . . . . 12
190189oveq2d 6077 . . . . . . . . . . 11
191190, 11syl6eq 2470 . . . . . . . . . 10
192187oveq2d 6077 . . . . . . . . . 10
193191, 192oveq12d 6079 . . . . . . . . 9
194193oveq2d 6077 . . . . . . . 8
195192oveq1d 6076 . . . . . . . . . . 11
196195oveq2d 6077 . . . . . . . . . 10
197191, 196oveq12d 6079 . . . . . . . . 9
198197oveq2d 6077 . . . . . . . 8
199188, 194, 198ifbieq12d 3793 . . . . . . 7
200199fveq2d 5665 . . . . . 6
201 fvex 5671 . . . . . 6
202200, 30, 201ovmpt2a 6191 . . . . 5
203102, 9, 202sylancl 647 . . . 4
20426fveq1i 5662 . . . . 5
205 fvex 5671 . . . . . . 7
206205fvconst2 5902 . . . . . 6
207206adantl 456 . . . . 5
208204, 207syl5eq 2466 . . . 4
209186, 203, 2083eqtr4d 2464 . . 3
210 simpl 447 . . . . . . . . . . 11
211210, 40syl6eqbr 4304 . . . . . . . . . 10
212 iftrue 3774 . . . . . . . . . 10
213211, 212syl 16 . . . . . . . . 9
214 simpr 451 . . . . . . . . . . . 12
215214oveq2d 6077 . . . . . . . . . . 11
216210oveq2d 6077 . . . . . . . . . . . 12
217 2t0e0 10423 . . . . . . . . . . . 12
218216, 217syl6eq 2470 . . . . . . . . . . 11
219215, 218oveq12d 6079 . . . . . . . . . 10
220219oveq2d 6077 . . . . . . . . 9
221213, 220eqtrd 2454 . . . . . . . 8