Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem8 Structured version   Visualization version   GIF version
Theorem cvmliftlem8 34581
Description: Lemma for cvmlift 34588. The functions 𝑄 are continuous functions because they are defined as β—‘(𝐹 β†Ύ 𝐼) ∘ 𝐺 where 𝐺 is continuous and (𝐹 β†Ύ 𝐼) is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.)
Hypotheses
Ref Expression
cvmliftlem.1 𝑆 = (π‘˜ ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑠 = (◑𝐹 β€œ π‘˜) ∧ βˆ€π‘’ ∈ 𝑠 (βˆ€π‘£ ∈ (𝑠 βˆ– {𝑒})(𝑒 ∩ 𝑣) = βˆ… ∧ (𝐹 β†Ύ 𝑒) ∈ ((𝐢 β†Ύt 𝑒)Homeo(𝐽 β†Ύt π‘˜))))})
cvmliftlem.b 𝐡 = βˆͺ 𝐢
cvmliftlem.x 𝑋 = βˆͺ 𝐽
cvmliftlem.f (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
cvmliftlem.g (πœ‘ β†’ 𝐺 ∈ (II Cn 𝐽))
cvmliftlem.p (πœ‘ β†’ 𝑃 ∈ 𝐡)
cvmliftlem.e (πœ‘ β†’ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))
cvmliftlem.n (πœ‘ β†’ 𝑁 ∈ β„•)
cvmliftlem.t (πœ‘ β†’ 𝑇:(1...𝑁)⟢βˆͺ 𝑗 ∈ 𝐽 ({𝑗} Γ— (π‘†β€˜π‘—)))
cvmliftlem.a (πœ‘ β†’ βˆ€π‘˜ ∈ (1...𝑁)(𝐺 β€œ (((π‘˜ βˆ’ 1) / 𝑁)[,](π‘˜ / 𝑁))) βŠ† (1st β€˜(π‘‡β€˜π‘˜)))
cvmliftlem.l 𝐿 = (topGenβ€˜ran (,))
cvmliftlem.q 𝑄 = seq0((π‘₯ ∈ V, π‘š ∈ β„• ↦ (𝑧 ∈ (((π‘š βˆ’ 1) / 𝑁)[,](π‘š / 𝑁)) ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘š))(π‘₯β€˜((π‘š βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§)))), (( I β†Ύ β„•) βˆͺ {⟨0, {⟨0, π‘ƒβŸ©}⟩}))
cvmliftlem5.3 π‘Š = (((𝑀 βˆ’ 1) / 𝑁)[,](𝑀 / 𝑁))
Assertion
Ref Expression
cvmliftlem8 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (π‘„β€˜π‘€) ∈ ((𝐿 β†Ύt π‘Š) Cn 𝐢))
Distinct variable groups:   𝑣,𝑏,𝑧,𝐡   𝑗,𝑏,π‘˜,π‘š,𝑠,𝑒,π‘₯,𝐹,𝑣,𝑧   𝑧,𝐿   𝑀,𝑏,𝑗,π‘˜,π‘š,𝑠,𝑒,𝑣,π‘₯,𝑧   𝑃,𝑏,π‘˜,π‘š,𝑒,𝑣,π‘₯,𝑧   𝐢,𝑏,𝑗,π‘˜,𝑠,𝑒,𝑣,𝑧   πœ‘,𝑗,𝑠,π‘₯,𝑧   𝑁,𝑏,π‘˜,π‘š,𝑒,𝑣,π‘₯,𝑧   𝑆,𝑏,𝑗,π‘˜,𝑠,𝑒,𝑣,π‘₯,𝑧   𝑗,𝑋   𝐺,𝑏,𝑗,π‘˜,π‘š,𝑠,𝑒,𝑣,π‘₯,𝑧   𝑇,𝑏,𝑗,π‘˜,π‘š,𝑠,𝑒,𝑣,π‘₯,𝑧   𝐽,𝑏,𝑗,π‘˜,𝑠,𝑒,𝑣,π‘₯,𝑧   𝑄,𝑏,π‘˜,π‘š,𝑒,𝑣,π‘₯,𝑧   π‘˜,π‘Š,π‘š,π‘₯,𝑧
Allowed substitution hints:   πœ‘(𝑣,𝑒,π‘˜,π‘š,𝑏)   𝐡(π‘₯,𝑒,𝑗,π‘˜,π‘š,𝑠)   𝐢(π‘₯,π‘š)   𝑃(𝑗,𝑠)   𝑄(𝑗,𝑠)   𝑆(π‘š)   𝐽(π‘š)   𝐿(π‘₯,𝑣,𝑒,𝑗,π‘˜,π‘š,𝑠,𝑏)   𝑁(𝑗,𝑠)   π‘Š(𝑣,𝑒,𝑗,𝑠,𝑏)   𝑋(π‘₯,𝑧,𝑣,𝑒,π‘˜,π‘š,𝑠,𝑏)
Proof of Theorem cvmliftlem8
StepHypRef Expression
1 elfznn 13534 . . 3 (𝑀 ∈ (1...𝑁) β†’ 𝑀 ∈ β„•)
2 cvmliftlem.1 . . . 4 𝑆 = (π‘˜ ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑠 = (◑𝐹 β€œ π‘˜) ∧ βˆ€π‘’ ∈ 𝑠 (βˆ€π‘£ ∈ (𝑠 βˆ– {𝑒})(𝑒 ∩ 𝑣) = βˆ… ∧ (𝐹 β†Ύ 𝑒) ∈ ((𝐢 β†Ύt 𝑒)Homeo(𝐽 β†Ύt π‘˜))))})
3 cvmliftlem.b . . . 4 𝐡 = βˆͺ 𝐢
4 cvmliftlem.x . . . 4 𝑋 = βˆͺ 𝐽
5 cvmliftlem.f . . . 4 (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
6 cvmliftlem.g . . . 4 (πœ‘ β†’ 𝐺 ∈ (II Cn 𝐽))
7 cvmliftlem.p . . . 4 (πœ‘ β†’ 𝑃 ∈ 𝐡)
8 cvmliftlem.e . . . 4 (πœ‘ β†’ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))
9 cvmliftlem.n . . . 4 (πœ‘ β†’ 𝑁 ∈ β„•)
10 cvmliftlem.t . . . 4 (πœ‘ β†’ 𝑇:(1...𝑁)⟢βˆͺ 𝑗 ∈ 𝐽 ({𝑗} Γ— (π‘†β€˜π‘—)))
11 cvmliftlem.a . . . 4 (πœ‘ β†’ βˆ€π‘˜ ∈ (1...𝑁)(𝐺 β€œ (((π‘˜ βˆ’ 1) / 𝑁)[,](π‘˜ / 𝑁))) βŠ† (1st β€˜(π‘‡β€˜π‘˜)))
12 cvmliftlem.l . . . 4 𝐿 = (topGenβ€˜ran (,))
13 cvmliftlem.q . . . 4 𝑄 = seq0((π‘₯ ∈ V, π‘š ∈ β„• ↦ (𝑧 ∈ (((π‘š βˆ’ 1) / 𝑁)[,](π‘š / 𝑁)) ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘š))(π‘₯β€˜((π‘š βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§)))), (( I β†Ύ β„•) βˆͺ {⟨0, {⟨0, π‘ƒβŸ©}⟩}))
14 cvmliftlem5.3 . . . 4 π‘Š = (((𝑀 βˆ’ 1) / 𝑁)[,](𝑀 / 𝑁))
152, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14cvmliftlem5 34578 . . 3 ((πœ‘ ∧ 𝑀 ∈ β„•) β†’ (π‘„β€˜π‘€) = (𝑧 ∈ π‘Š ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§))))
161, 15sylan2 591 . 2 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (π‘„β€˜π‘€) = (𝑧 ∈ π‘Š ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§))))
175adantr 479 . . . 4 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
18 cvmtop1 34549 . . . 4 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐢 ∈ Top)
19 cnrest2r 23011 . . . 4 (𝐢 ∈ Top β†’ ((𝐿 β†Ύt π‘Š) Cn (𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))) βŠ† ((𝐿 β†Ύt π‘Š) Cn 𝐢))
2017, 18, 193syl 18 . . 3 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝐿 β†Ύt π‘Š) Cn (𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))) βŠ† ((𝐿 β†Ύt π‘Š) Cn 𝐢))
21 retopon 24500 . . . . . 6 (topGenβ€˜ran (,)) ∈ (TopOnβ€˜β„)
2212, 21eqeltri 2827 . . . . 5 𝐿 ∈ (TopOnβ€˜β„)
23 simpr 483 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝑀 ∈ (1...𝑁))
242, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14cvmliftlem2 34575 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ π‘Š βŠ† (0[,]1))
25 unitssre 13480 . . . . . 6 (0[,]1) βŠ† ℝ
2624, 25sstrdi 3993 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ π‘Š βŠ† ℝ)
27 resttopon 22885 . . . . 5 ((𝐿 ∈ (TopOnβ€˜β„) ∧ π‘Š βŠ† ℝ) β†’ (𝐿 β†Ύt π‘Š) ∈ (TopOnβ€˜π‘Š))
2822, 26, 27sylancr 585 . . . 4 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝐿 β†Ύt π‘Š) ∈ (TopOnβ€˜π‘Š))
29 eqid 2730 . . . . . . 7 (II β†Ύt π‘Š) = (II β†Ύt π‘Š)
30 iitopon 24619 . . . . . . . 8 II ∈ (TopOnβ€˜(0[,]1))
3130a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ II ∈ (TopOnβ€˜(0[,]1)))
326adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐺 ∈ (II Cn 𝐽))
33 iiuni 24621 . . . . . . . . . . 11 (0[,]1) = βˆͺ II
3433, 4cnf 22970 . . . . . . . . . 10 (𝐺 ∈ (II Cn 𝐽) β†’ 𝐺:(0[,]1)βŸΆπ‘‹)
3532, 34syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐺:(0[,]1)βŸΆπ‘‹)
3635feqmptd 6959 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐺 = (𝑧 ∈ (0[,]1) ↦ (πΊβ€˜π‘§)))
3736, 32eqeltrrd 2832 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑧 ∈ (0[,]1) ↦ (πΊβ€˜π‘§)) ∈ (II Cn 𝐽))
3829, 31, 24, 37cnmpt1res 23400 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) ∈ ((II β†Ύt π‘Š) Cn 𝐽))
39 dfii2 24622 . . . . . . . . . 10 II = ((topGenβ€˜ran (,)) β†Ύt (0[,]1))
4012oveq1i 7421 . . . . . . . . . 10 (𝐿 β†Ύt (0[,]1)) = ((topGenβ€˜ran (,)) β†Ύt (0[,]1))
4139, 40eqtr4i 2761 . . . . . . . . 9 II = (𝐿 β†Ύt (0[,]1))
4241oveq1i 7421 . . . . . . . 8 (II β†Ύt π‘Š) = ((𝐿 β†Ύt (0[,]1)) β†Ύt π‘Š)
43 retop 24498 . . . . . . . . . . 11 (topGenβ€˜ran (,)) ∈ Top
4412, 43eqeltri 2827 . . . . . . . . . 10 𝐿 ∈ Top
4544a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐿 ∈ Top)
46 ovexd 7446 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (0[,]1) ∈ V)
47 restabs 22889 . . . . . . . . 9 ((𝐿 ∈ Top ∧ π‘Š βŠ† (0[,]1) ∧ (0[,]1) ∈ V) β†’ ((𝐿 β†Ύt (0[,]1)) β†Ύt π‘Š) = (𝐿 β†Ύt π‘Š))
4845, 24, 46, 47syl3anc 1369 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝐿 β†Ύt (0[,]1)) β†Ύt π‘Š) = (𝐿 β†Ύt π‘Š))
4942, 48eqtrid 2782 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (II β†Ύt π‘Š) = (𝐿 β†Ύt π‘Š))
5049oveq1d 7426 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((II β†Ύt π‘Š) Cn 𝐽) = ((𝐿 β†Ύt π‘Š) Cn 𝐽))
5138, 50eleqtrd 2833 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) ∈ ((𝐿 β†Ύt π‘Š) Cn 𝐽))
52 cvmtop2 34550 . . . . . . . 8 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐽 ∈ Top)
5317, 52syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐽 ∈ Top)
544toptopon 22639 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
5553, 54sylib 217 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
56 simprl 767 . . . . . . . . . 10 ((πœ‘ ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧 ∈ π‘Š)) β†’ 𝑀 ∈ (1...𝑁))
57 simprr 769 . . . . . . . . . 10 ((πœ‘ ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧 ∈ π‘Š)) β†’ 𝑧 ∈ π‘Š)
582, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 56, 14, 57cvmliftlem3 34576 . . . . . . . . 9 ((πœ‘ ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧 ∈ π‘Š)) β†’ (πΊβ€˜π‘§) ∈ (1st β€˜(π‘‡β€˜π‘€)))
5958anassrs 466 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) ∧ 𝑧 ∈ π‘Š) β†’ (πΊβ€˜π‘§) ∈ (1st β€˜(π‘‡β€˜π‘€)))
6059fmpttd 7115 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)):π‘ŠβŸΆ(1st β€˜(π‘‡β€˜π‘€)))
6160frnd 6724 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ran (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) βŠ† (1st β€˜(π‘‡β€˜π‘€)))
622, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23cvmliftlem1 34574 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (2nd β€˜(π‘‡β€˜π‘€)) ∈ (π‘†β€˜(1st β€˜(π‘‡β€˜π‘€))))
632cvmsrcl 34553 . . . . . . . 8 ((2nd β€˜(π‘‡β€˜π‘€)) ∈ (π‘†β€˜(1st β€˜(π‘‡β€˜π‘€))) β†’ (1st β€˜(π‘‡β€˜π‘€)) ∈ 𝐽)
64 elssuni 4940 . . . . . . . 8 ((1st β€˜(π‘‡β€˜π‘€)) ∈ 𝐽 β†’ (1st β€˜(π‘‡β€˜π‘€)) βŠ† βˆͺ 𝐽)
6562, 63, 643syl 18 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (1st β€˜(π‘‡β€˜π‘€)) βŠ† βˆͺ 𝐽)
6665, 4sseqtrrdi 4032 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (1st β€˜(π‘‡β€˜π‘€)) βŠ† 𝑋)
67 cnrest2 23010 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ ran (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) βŠ† (1st β€˜(π‘‡β€˜π‘€)) ∧ (1st β€˜(π‘‡β€˜π‘€)) βŠ† 𝑋) β†’ ((𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) ∈ ((𝐿 β†Ύt π‘Š) Cn 𝐽) ↔ (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) ∈ ((𝐿 β†Ύt π‘Š) Cn (𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€))))))
6855, 61, 66, 67syl3anc 1369 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) ∈ ((𝐿 β†Ύt π‘Š) Cn 𝐽) ↔ (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) ∈ ((𝐿 β†Ύt π‘Š) Cn (𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€))))))
6951, 68mpbid 231 . . . 4 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑧 ∈ π‘Š ↦ (πΊβ€˜π‘§)) ∈ ((𝐿 β†Ύt π‘Š) Cn (𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€)))))
702, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14cvmliftlem7 34580 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ (◑𝐹 β€œ {(πΊβ€˜((𝑀 βˆ’ 1) / 𝑁))}))
71 cvmcn 34551 . . . . . . . . . . . 12 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐹 ∈ (𝐢 Cn 𝐽))
723, 4cnf 22970 . . . . . . . . . . . 12 (𝐹 ∈ (𝐢 Cn 𝐽) β†’ 𝐹:π΅βŸΆπ‘‹)
7317, 71, 723syl 18 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝐹:π΅βŸΆπ‘‹)
74 ffn 6716 . . . . . . . . . . 11 (𝐹:π΅βŸΆπ‘‹ β†’ 𝐹 Fn 𝐡)
75 fniniseg 7060 . . . . . . . . . . 11 (𝐹 Fn 𝐡 β†’ (((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ (◑𝐹 β€œ {(πΊβ€˜((𝑀 βˆ’ 1) / 𝑁))}) ↔ (((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝐡 ∧ (πΉβ€˜((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁))) = (πΊβ€˜((𝑀 βˆ’ 1) / 𝑁)))))
7673, 74, 753syl 18 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ (◑𝐹 β€œ {(πΊβ€˜((𝑀 βˆ’ 1) / 𝑁))}) ↔ (((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝐡 ∧ (πΉβ€˜((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁))) = (πΊβ€˜((𝑀 βˆ’ 1) / 𝑁)))))
7770, 76mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝐡 ∧ (πΉβ€˜((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁))) = (πΊβ€˜((𝑀 βˆ’ 1) / 𝑁))))
7877simpld 493 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝐡)
7977simprd 494 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (πΉβ€˜((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁))) = (πΊβ€˜((𝑀 βˆ’ 1) / 𝑁)))
801adantl 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝑀 ∈ β„•)
8180nnred 12231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝑀 ∈ ℝ)
82 peano2rem 11531 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℝ β†’ (𝑀 βˆ’ 1) ∈ ℝ)
8381, 82syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑀 βˆ’ 1) ∈ ℝ)
849adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝑁 ∈ β„•)
8583, 84nndivred 12270 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑀 βˆ’ 1) / 𝑁) ∈ ℝ)
8685rexrd 11268 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑀 βˆ’ 1) / 𝑁) ∈ ℝ*)
8781, 84nndivred 12270 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑀 / 𝑁) ∈ ℝ)
8887rexrd 11268 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑀 / 𝑁) ∈ ℝ*)
8981ltm1d 12150 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑀 βˆ’ 1) < 𝑀)
9084nnred 12231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 𝑁 ∈ ℝ)
9184nngt0d 12265 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ 0 < 𝑁)
92 ltdiv1 12082 . . . . . . . . . . . . . . 15 (((𝑀 βˆ’ 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ ((𝑀 βˆ’ 1) < 𝑀 ↔ ((𝑀 βˆ’ 1) / 𝑁) < (𝑀 / 𝑁)))
9383, 81, 90, 91, 92syl112anc 1372 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑀 βˆ’ 1) < 𝑀 ↔ ((𝑀 βˆ’ 1) / 𝑁) < (𝑀 / 𝑁)))
9489, 93mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑀 βˆ’ 1) / 𝑁) < (𝑀 / 𝑁))
9585, 87, 94ltled 11366 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑀 βˆ’ 1) / 𝑁) ≀ (𝑀 / 𝑁))
96 lbicc2 13445 . . . . . . . . . . . 12 ((((𝑀 βˆ’ 1) / 𝑁) ∈ ℝ* ∧ (𝑀 / 𝑁) ∈ ℝ* ∧ ((𝑀 βˆ’ 1) / 𝑁) ≀ (𝑀 / 𝑁)) β†’ ((𝑀 βˆ’ 1) / 𝑁) ∈ (((𝑀 βˆ’ 1) / 𝑁)[,](𝑀 / 𝑁)))
9786, 88, 95, 96syl3anc 1369 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑀 βˆ’ 1) / 𝑁) ∈ (((𝑀 βˆ’ 1) / 𝑁)[,](𝑀 / 𝑁)))
9897, 14eleqtrrdi 2842 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((𝑀 βˆ’ 1) / 𝑁) ∈ π‘Š)
992, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14, 98cvmliftlem3 34576 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (πΊβ€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ (1st β€˜(π‘‡β€˜π‘€)))
10079, 99eqeltrd 2831 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (πΉβ€˜((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁))) ∈ (1st β€˜(π‘‡β€˜π‘€)))
101 eqid 2730 . . . . . . . . 9 (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏) = (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)
1022, 3, 101cvmsiota 34566 . . . . . . . 8 ((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ ((2nd β€˜(π‘‡β€˜π‘€)) ∈ (π‘†β€˜(1st β€˜(π‘‡β€˜π‘€))) ∧ ((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝐡 ∧ (πΉβ€˜((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁))) ∈ (1st β€˜(π‘‡β€˜π‘€)))) β†’ ((℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏) ∈ (2nd β€˜(π‘‡β€˜π‘€)) ∧ ((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)))
10317, 62, 78, 100, 102syl13anc 1370 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ ((℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏) ∈ (2nd β€˜(π‘‡β€˜π‘€)) ∧ ((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)))
104103simpld 493 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏) ∈ (2nd β€˜(π‘‡β€˜π‘€)))
1052cvmshmeo 34560 . . . . . 6 (((2nd β€˜(π‘‡β€˜π‘€)) ∈ (π‘†β€˜(1st β€˜(π‘‡β€˜π‘€))) ∧ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏) ∈ (2nd β€˜(π‘‡β€˜π‘€))) β†’ (𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€)))))
10662, 104, 105syl2anc 582 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€)))))
107 hmeocnvcn 23485 . . . . 5 ((𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€)))) β†’ β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€))) Cn (𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))))
108106, 107syl 17 . . . 4 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐽 β†Ύt (1st β€˜(π‘‡β€˜π‘€))) Cn (𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))))
10928, 69, 108cnmpt11f 23388 . . 3 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑧 ∈ π‘Š ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§))) ∈ ((𝐿 β†Ύt π‘Š) Cn (𝐢 β†Ύt (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))))
11020, 109sseldd 3982 . 2 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (𝑧 ∈ π‘Š ↦ (β—‘(𝐹 β†Ύ (℩𝑏 ∈ (2nd β€˜(π‘‡β€˜π‘€))((π‘„β€˜(𝑀 βˆ’ 1))β€˜((𝑀 βˆ’ 1) / 𝑁)) ∈ 𝑏))β€˜(πΊβ€˜π‘§))) ∈ ((𝐿 β†Ύt π‘Š) Cn 𝐢))
11116, 110eqeltrd 2831 1 ((πœ‘ ∧ 𝑀 ∈ (1...𝑁)) β†’ (π‘„β€˜π‘€) ∈ ((𝐿 β†Ύt π‘Š) Cn 𝐢))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  {crab 3430  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907  βˆͺ ciun 4996   class class class wbr 5147   ↦ cmpt 5230   I cid 5572   Γ— cxp 5673  β—‘ccnv 5674  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  β„©crio 7366  (class class class)co 7411   ∈ cmpo 7413  1st c1st 7975  2nd c2nd 7976  β„cr 11111  0cc0 11112  1c1 11113  β„*cxr 11251   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448   / cdiv 11875  β„•cn 12216  (,)cioo 13328  [,]cicc 13331  ...cfz 13488  seqcseq 13970   β†Ύt crest 17370  topGenctg 17387  Topctop 22615  TopOnctopon 22632   Cn ccn 22948  Homeochmeo 23477  IIcii 24615   CovMap ccvm 34544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-icc 13335  df-fz 13489  df-seq 13971  df-exp 14032  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-rest 17372  df-topgen 17393  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-top 22616  df-topon 22633  df-bases 22669  df-cn 22951  df-hmeo 23479  df-ii 24617  df-cvm 34545
This theorem is referenced by:  cvmliftlem10  34583
  Copyright terms: Public domain W3C validator