Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem8 Structured version   Visualization version   GIF version

Theorem cvmliftlem8 31581
 Description: Lemma for cvmlift 31588. 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 12563 . . 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 31578 . . 3 ((𝜑𝑀 ∈ ℕ) → (𝑄𝑀) = (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))))
161, 15sylan2 492 . 2 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑄𝑀) = (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))))
175adantr 472 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
18 cvmtop1 31549 . . . 4 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
19 cnrest2r 21293 . . . 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 22768 . . . . . 6 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
2212, 21eqeltri 2835 . . . . 5 𝐿 ∈ (TopOn‘ℝ)
23 simpr 479 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
242, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14cvmliftlem2 31575 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑊 ⊆ (0[,]1))
25 unitssre 12512 . . . . . 6 (0[,]1) ⊆ ℝ
2624, 25syl6ss 3756 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑊 ⊆ ℝ)
27 resttopon 21167 . . . . 5 ((𝐿 ∈ (TopOn‘ℝ) ∧ 𝑊 ⊆ ℝ) → (𝐿t 𝑊) ∈ (TopOn‘𝑊))
2822, 26, 27sylancr 698 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐿t 𝑊) ∈ (TopOn‘𝑊))
29 eqid 2760 . . . . . . 7 (II ↾t 𝑊) = (II ↾t 𝑊)
30 iitopon 22883 . . . . . . . 8 II ∈ (TopOn‘(0[,]1))
3130a1i 11 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → II ∈ (TopOn‘(0[,]1)))
326adantr 472 . . . . . . . . . 10 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐺 ∈ (II Cn 𝐽))
33 iiuni 22885 . . . . . . . . . . 11 (0[,]1) = II
3433, 4cnf 21252 . . . . . . . . . 10 (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋)
3532, 34syl 17 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐺:(0[,]1)⟶𝑋)
3635feqmptd 6411 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐺 = (𝑧 ∈ (0[,]1) ↦ (𝐺𝑧)))
3736, 32eqeltrrd 2840 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧 ∈ (0[,]1) ↦ (𝐺𝑧)) ∈ (II Cn 𝐽))
3829, 31, 24, 37cnmpt1res 21681 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((II ↾t 𝑊) Cn 𝐽))
39 dfii2 22886 . . . . . . . . . 10 II = ((topGen‘ran (,)) ↾t (0[,]1))
4012oveq1i 6823 . . . . . . . . . 10 (𝐿t (0[,]1)) = ((topGen‘ran (,)) ↾t (0[,]1))
4139, 40eqtr4i 2785 . . . . . . . . 9 II = (𝐿t (0[,]1))
4241oveq1i 6823 . . . . . . . 8 (II ↾t 𝑊) = ((𝐿t (0[,]1)) ↾t 𝑊)
43 retop 22766 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
4412, 43eqeltri 2835 . . . . . . . . . 10 𝐿 ∈ Top
4544a1i 11 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐿 ∈ Top)
46 ovexd 6843 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (0[,]1) ∈ V)
47 restabs 21171 . . . . . . . . 9 ((𝐿 ∈ Top ∧ 𝑊 ⊆ (0[,]1) ∧ (0[,]1) ∈ V) → ((𝐿t (0[,]1)) ↾t 𝑊) = (𝐿t 𝑊))
4845, 24, 46, 47syl3anc 1477 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝐿t (0[,]1)) ↾t 𝑊) = (𝐿t 𝑊))
4942, 48syl5eq 2806 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (II ↾t 𝑊) = (𝐿t 𝑊))
5049oveq1d 6828 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → ((II ↾t 𝑊) Cn 𝐽) = ((𝐿t 𝑊) Cn 𝐽))
5138, 50eleqtrd 2841 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn 𝐽))
52 cvmtop2 31550 . . . . . . . 8 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
5317, 52syl 17 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐽 ∈ Top)
544toptopon 20924 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
5553, 54sylib 208 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐽 ∈ (TopOn‘𝑋))
56 simprl 811 . . . . . . . . . 10 ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧𝑊)) → 𝑀 ∈ (1...𝑁))
57 simprr 813 . . . . . . . . . 10 ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧𝑊)) → 𝑧𝑊)
582, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 56, 14, 57cvmliftlem3 31576 . . . . . . . . 9 ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧𝑊)) → (𝐺𝑧) ∈ (1st ‘(𝑇𝑀)))
5958anassrs 683 . . . . . . . 8 (((𝜑𝑀 ∈ (1...𝑁)) ∧ 𝑧𝑊) → (𝐺𝑧) ∈ (1st ‘(𝑇𝑀)))
60 eqid 2760 . . . . . . . 8 (𝑧𝑊 ↦ (𝐺𝑧)) = (𝑧𝑊 ↦ (𝐺𝑧))
6159, 60fmptd 6548 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)):𝑊⟶(1st ‘(𝑇𝑀)))
62 frn 6214 . . . . . . 7 ((𝑧𝑊 ↦ (𝐺𝑧)):𝑊⟶(1st ‘(𝑇𝑀)) → ran (𝑧𝑊 ↦ (𝐺𝑧)) ⊆ (1st ‘(𝑇𝑀)))
6361, 62syl 17 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → ran (𝑧𝑊 ↦ (𝐺𝑧)) ⊆ (1st ‘(𝑇𝑀)))
642, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23cvmliftlem1 31574 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → (2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))))
652cvmsrcl 31553 . . . . . . . 8 ((2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))) → (1st ‘(𝑇𝑀)) ∈ 𝐽)
66 elssuni 4619 . . . . . . . 8 ((1st ‘(𝑇𝑀)) ∈ 𝐽 → (1st ‘(𝑇𝑀)) ⊆ 𝐽)
6764, 65, 663syl 18 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (1st ‘(𝑇𝑀)) ⊆ 𝐽)
6867, 4syl6sseqr 3793 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → (1st ‘(𝑇𝑀)) ⊆ 𝑋)
69 cnrest2 21292 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ ran (𝑧𝑊 ↦ (𝐺𝑧)) ⊆ (1st ‘(𝑇𝑀)) ∧ (1st ‘(𝑇𝑀)) ⊆ 𝑋) → ((𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn 𝐽) ↔ (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn (𝐽t (1st ‘(𝑇𝑀))))))
7055, 63, 68, 69syl3anc 1477 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn 𝐽) ↔ (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn (𝐽t (1st ‘(𝑇𝑀))))))
7151, 70mpbid 222 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn (𝐽t (1st ‘(𝑇𝑀)))))
722, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14cvmliftlem7 31580 . . . . . . . . . 10 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
73 cvmcn 31551 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
743, 4cnf 21252 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵𝑋)
7517, 73, 743syl 18 . . . . . . . . . . 11 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐹:𝐵𝑋)
76 ffn 6206 . . . . . . . . . . 11 (𝐹:𝐵𝑋𝐹 Fn 𝐵)
77 fniniseg 6501 . . . . . . . . . . 11 (𝐹 Fn 𝐵 → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}) ↔ (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))))
7875, 76, 773syl 18 . . . . . . . . . 10 ((𝜑𝑀 ∈ (1...𝑁)) → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}) ↔ (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))))
7972, 78mpbid 222 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁))))
8079simpld 477 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵)
8179simprd 482 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))
821adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑀 ∈ ℕ)
8382nnred 11227 . . . . . . . . . . . . . . 15 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑀 ∈ ℝ)
84 peano2rem 10540 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
8583, 84syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ ℝ)
869adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℕ)
8785, 86nndivred 11261 . . . . . . . . . . . . 13 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ ℝ)
8887rexrd 10281 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ ℝ*)
8983, 86nndivred 11261 . . . . . . . . . . . . 13 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 / 𝑁) ∈ ℝ)
9089rexrd 10281 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 / 𝑁) ∈ ℝ*)
9183ltm1d 11148 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 − 1) < 𝑀)
9286nnred 11227 . . . . . . . . . . . . . . 15 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℝ)
9386nngt0d 11256 . . . . . . . . . . . . . . 15 ((𝜑𝑀 ∈ (1...𝑁)) → 0 < 𝑁)
94 ltdiv1 11079 . . . . . . . . . . . . . . 15 (((𝑀 − 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁)))
9585, 83, 92, 93, 94syl112anc 1481 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁)))
9691, 95mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁))
9787, 89, 96ltled 10377 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁))
98 lbicc2 12481 . . . . . . . . . . . 12 ((((𝑀 − 1) / 𝑁) ∈ ℝ* ∧ (𝑀 / 𝑁) ∈ ℝ* ∧ ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)))
9988, 90, 97, 98syl3anc 1477 . . . . . . . . . . 11 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)))
10099, 14syl6eleqr 2850 . . . . . . . . . 10 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ 𝑊)
1012, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14, 100cvmliftlem3 31576 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐺‘((𝑀 − 1) / 𝑁)) ∈ (1st ‘(𝑇𝑀)))
10281, 101eqeltrd 2839 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1st ‘(𝑇𝑀)))
103 eqid 2760 . . . . . . . . 9 (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) = (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)
1042, 3, 103cvmsiota 31566 . . . . . . . 8 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ ((2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1st ‘(𝑇𝑀)))) → ((𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))
10517, 64, 80, 102, 104syl13anc 1479 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))
106105simpld 477 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀)))
1072cvmshmeo 31560 . . . . . 6 (((2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))) ∧ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀))) → (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽t (1st ‘(𝑇𝑀)))))
10864, 106, 107syl2anc 696 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽t (1st ‘(𝑇𝑀)))))
109 hmeocnvcn 21766 . . . . 5 ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽t (1st ‘(𝑇𝑀)))) → (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐽t (1st ‘(𝑇𝑀))) Cn (𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))))
110108, 109syl 17 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐽t (1st ‘(𝑇𝑀))) Cn (𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))))
11128, 71, 110cnmpt11f 21669 . . 3 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))) ∈ ((𝐿t 𝑊) Cn (𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))))
11220, 111sseldd 3745 . 2 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))) ∈ ((𝐿t 𝑊) Cn 𝐶))
11316, 112eqeltrd 2839 1 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑄𝑀) ∈ ((𝐿t 𝑊) Cn 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∀wral 3050  {crab 3054  Vcvv 3340   ∖ cdif 3712   ∪ cun 3713   ∩ cin 3714   ⊆ wss 3715  ∅c0 4058  𝒫 cpw 4302  {csn 4321  ⟨cop 4327  ∪ cuni 4588  ∪ ciun 4672   class class class wbr 4804   ↦ cmpt 4881   I cid 5173   × cxp 5264  ◡ccnv 5265  ran crn 5267   ↾ cres 5268   “ cima 5269   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  ℩crio 6773  (class class class)co 6813   ↦ cmpt2 6815  1st c1st 7331  2nd c2nd 7332  ℝcr 10127  0cc0 10128  1c1 10129  ℝ*cxr 10265   < clt 10266   ≤ cle 10267   − cmin 10458   / cdiv 10876  ℕcn 11212  (,)cioo 12368  [,]cicc 12371  ...cfz 12519  seqcseq 12995   ↾t crest 16283  topGenctg 16300  Topctop 20900  TopOnctopon 20917   Cn ccn 21230  Homeochmeo 21758  IIcii 22879   CovMap ccvm 31544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fi 8482  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-z 11570  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-icc 12375  df-fz 12520  df-seq 12996  df-exp 13055  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-rest 16285  df-topgen 16306  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-top 20901  df-topon 20918  df-bases 20952  df-cn 21233  df-hmeo 21760  df-ii 22881  df-cvm 31545 This theorem is referenced by:  cvmliftlem10  31583
 Copyright terms: Public domain W3C validator