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

Theorem cvmliftlem8 32667
 Description: Lemma for cvmlift 32674. 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 12934 . . 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 32664 . . 3 ((𝜑𝑀 ∈ ℕ) → (𝑄𝑀) = (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))))
161, 15sylan2 595 . 2 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑄𝑀) = (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))))
175adantr 484 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
18 cvmtop1 32635 . . . 4 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
19 cnrest2r 21902 . . . 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 23379 . . . . . 6 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
2212, 21eqeltri 2886 . . . . 5 𝐿 ∈ (TopOn‘ℝ)
23 simpr 488 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
242, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14cvmliftlem2 32661 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑊 ⊆ (0[,]1))
25 unitssre 12880 . . . . . 6 (0[,]1) ⊆ ℝ
2624, 25sstrdi 3927 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑊 ⊆ ℝ)
27 resttopon 21776 . . . . 5 ((𝐿 ∈ (TopOn‘ℝ) ∧ 𝑊 ⊆ ℝ) → (𝐿t 𝑊) ∈ (TopOn‘𝑊))
2822, 26, 27sylancr 590 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐿t 𝑊) ∈ (TopOn‘𝑊))
29 eqid 2798 . . . . . . 7 (II ↾t 𝑊) = (II ↾t 𝑊)
30 iitopon 23494 . . . . . . . 8 II ∈ (TopOn‘(0[,]1))
3130a1i 11 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → II ∈ (TopOn‘(0[,]1)))
326adantr 484 . . . . . . . . . 10 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐺 ∈ (II Cn 𝐽))
33 iiuni 23496 . . . . . . . . . . 11 (0[,]1) = II
3433, 4cnf 21861 . . . . . . . . . 10 (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋)
3532, 34syl 17 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐺:(0[,]1)⟶𝑋)
3635feqmptd 6709 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐺 = (𝑧 ∈ (0[,]1) ↦ (𝐺𝑧)))
3736, 32eqeltrrd 2891 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧 ∈ (0[,]1) ↦ (𝐺𝑧)) ∈ (II Cn 𝐽))
3829, 31, 24, 37cnmpt1res 22291 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((II ↾t 𝑊) Cn 𝐽))
39 dfii2 23497 . . . . . . . . . 10 II = ((topGen‘ran (,)) ↾t (0[,]1))
4012oveq1i 7146 . . . . . . . . . 10 (𝐿t (0[,]1)) = ((topGen‘ran (,)) ↾t (0[,]1))
4139, 40eqtr4i 2824 . . . . . . . . 9 II = (𝐿t (0[,]1))
4241oveq1i 7146 . . . . . . . 8 (II ↾t 𝑊) = ((𝐿t (0[,]1)) ↾t 𝑊)
43 retop 23377 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
4412, 43eqeltri 2886 . . . . . . . . . 10 𝐿 ∈ Top
4544a1i 11 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐿 ∈ Top)
46 ovexd 7171 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (0[,]1) ∈ V)
47 restabs 21780 . . . . . . . . 9 ((𝐿 ∈ Top ∧ 𝑊 ⊆ (0[,]1) ∧ (0[,]1) ∈ V) → ((𝐿t (0[,]1)) ↾t 𝑊) = (𝐿t 𝑊))
4845, 24, 46, 47syl3anc 1368 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝐿t (0[,]1)) ↾t 𝑊) = (𝐿t 𝑊))
4942, 48syl5eq 2845 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (II ↾t 𝑊) = (𝐿t 𝑊))
5049oveq1d 7151 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → ((II ↾t 𝑊) Cn 𝐽) = ((𝐿t 𝑊) Cn 𝐽))
5138, 50eleqtrd 2892 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn 𝐽))
52 cvmtop2 32636 . . . . . . . 8 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
5317, 52syl 17 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐽 ∈ Top)
544toptopon 21532 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
5553, 54sylib 221 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐽 ∈ (TopOn‘𝑋))
56 simprl 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧𝑊)) → 𝑀 ∈ (1...𝑁))
57 simprr 772 . . . . . . . . . 10 ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧𝑊)) → 𝑧𝑊)
582, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 56, 14, 57cvmliftlem3 32662 . . . . . . . . 9 ((𝜑 ∧ (𝑀 ∈ (1...𝑁) ∧ 𝑧𝑊)) → (𝐺𝑧) ∈ (1st ‘(𝑇𝑀)))
5958anassrs 471 . . . . . . . 8 (((𝜑𝑀 ∈ (1...𝑁)) ∧ 𝑧𝑊) → (𝐺𝑧) ∈ (1st ‘(𝑇𝑀)))
6059fmpttd 6857 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)):𝑊⟶(1st ‘(𝑇𝑀)))
6160frnd 6495 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → ran (𝑧𝑊 ↦ (𝐺𝑧)) ⊆ (1st ‘(𝑇𝑀)))
622, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23cvmliftlem1 32660 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → (2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))))
632cvmsrcl 32639 . . . . . . . 8 ((2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))) → (1st ‘(𝑇𝑀)) ∈ 𝐽)
64 elssuni 4831 . . . . . . . 8 ((1st ‘(𝑇𝑀)) ∈ 𝐽 → (1st ‘(𝑇𝑀)) ⊆ 𝐽)
6562, 63, 643syl 18 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → (1st ‘(𝑇𝑀)) ⊆ 𝐽)
6665, 4sseqtrrdi 3966 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → (1st ‘(𝑇𝑀)) ⊆ 𝑋)
67 cnrest2 21901 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ ran (𝑧𝑊 ↦ (𝐺𝑧)) ⊆ (1st ‘(𝑇𝑀)) ∧ (1st ‘(𝑇𝑀)) ⊆ 𝑋) → ((𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn 𝐽) ↔ (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn (𝐽t (1st ‘(𝑇𝑀))))))
6855, 61, 66, 67syl3anc 1368 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn 𝐽) ↔ (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn (𝐽t (1st ‘(𝑇𝑀))))))
6951, 68mpbid 235 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ (𝐺𝑧)) ∈ ((𝐿t 𝑊) Cn (𝐽t (1st ‘(𝑇𝑀)))))
702, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14cvmliftlem7 32666 . . . . . . . . . 10 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
71 cvmcn 32637 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
723, 4cnf 21861 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵𝑋)
7317, 71, 723syl 18 . . . . . . . . . . 11 ((𝜑𝑀 ∈ (1...𝑁)) → 𝐹:𝐵𝑋)
74 ffn 6488 . . . . . . . . . . 11 (𝐹:𝐵𝑋𝐹 Fn 𝐵)
75 fniniseg 6808 . . . . . . . . . . 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 235 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁))))
7877simpld 498 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵)
7977simprd 499 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))
801adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑀 ∈ ℕ)
8180nnred 11643 . . . . . . . . . . . . . . 15 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑀 ∈ ℝ)
82 peano2rem 10945 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
8381, 82syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ ℝ)
849adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℕ)
8583, 84nndivred 11682 . . . . . . . . . . . . 13 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ ℝ)
8685rexrd 10683 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ ℝ*)
8781, 84nndivred 11682 . . . . . . . . . . . . 13 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 / 𝑁) ∈ ℝ)
8887rexrd 10683 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 / 𝑁) ∈ ℝ*)
8981ltm1d 11564 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 − 1) < 𝑀)
9084nnred 11643 . . . . . . . . . . . . . . 15 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℝ)
9184nngt0d 11677 . . . . . . . . . . . . . . 15 ((𝜑𝑀 ∈ (1...𝑁)) → 0 < 𝑁)
92 ltdiv1 11496 . . . . . . . . . . . . . . 15 (((𝑀 − 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁)))
9383, 81, 90, 91, 92syl112anc 1371 . . . . . . . . . . . . . 14 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁)))
9489, 93mpbid 235 . . . . . . . . . . . . 13 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁))
9585, 87, 94ltled 10780 . . . . . . . . . . . 12 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁))
96 lbicc2 12845 . . . . . . . . . . . 12 ((((𝑀 − 1) / 𝑁) ∈ ℝ* ∧ (𝑀 / 𝑁) ∈ ℝ* ∧ ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)))
9786, 88, 95, 96syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)))
9897, 14eleqtrrdi 2901 . . . . . . . . . 10 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑀 − 1) / 𝑁) ∈ 𝑊)
992, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14, 98cvmliftlem3 32662 . . . . . . . . 9 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐺‘((𝑀 − 1) / 𝑁)) ∈ (1st ‘(𝑇𝑀)))
10079, 99eqeltrd 2890 . . . . . . . 8 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1st ‘(𝑇𝑀)))
101 eqid 2798 . . . . . . . . 9 (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) = (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)
1022, 3, 101cvmsiota 32652 . . . . . . . 8 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ ((2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1st ‘(𝑇𝑀)))) → ((𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))
10317, 62, 78, 100, 102syl13anc 1369 . . . . . . 7 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))
104103simpld 498 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀)))
1052cvmshmeo 32646 . . . . . 6 (((2nd ‘(𝑇𝑀)) ∈ (𝑆‘(1st ‘(𝑇𝑀))) ∧ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2nd ‘(𝑇𝑀))) → (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽t (1st ‘(𝑇𝑀)))))
10662, 104, 105syl2anc 587 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → (𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) ∈ ((𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))Homeo(𝐽t (1st ‘(𝑇𝑀)))))
107 hmeocnvcn 22376 . . . . 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 22279 . . 3 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))) ∈ ((𝐿t 𝑊) Cn (𝐶t (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))))
11020, 109sseldd 3916 . 2 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑧𝑊 ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧))) ∈ ((𝐿t 𝑊) Cn 𝐶))
11116, 110eqeltrd 2890 1 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑄𝑀) ∈ ((𝐿t 𝑊) Cn 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ⟨cop 4531  ∪ cuni 4801  ∪ ciun 4882   class class class wbr 5031   ↦ cmpt 5111   I cid 5425   × cxp 5518  ◡ccnv 5519  ran crn 5521   ↾ cres 5522   “ cima 5523   Fn wfn 6320  ⟶wf 6321  ‘cfv 6325  ℩crio 7093  (class class class)co 7136   ∈ cmpo 7138  1st c1st 7672  2nd c2nd 7673  ℝcr 10528  0cc0 10529  1c1 10530  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℕcn 11628  (,)cioo 12729  [,]cicc 12732  ...cfz 12888  seqcseq 13367   ↾t crest 16689  topGenctg 16706  Topctop 21508  TopOnctopon 21525   Cn ccn 21839  Homeochmeo 22368  IIcii 23490   CovMap ccvm 32630 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-oadd 8092  df-er 8275  df-map 8394  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fi 8862  df-sup 8893  df-inf 8894  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-n0 11889  df-z 11973  df-uz 12235  df-q 12340  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-ioo 12733  df-icc 12736  df-fz 12889  df-seq 13368  df-exp 13429  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-rest 16691  df-topgen 16712  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-top 21509  df-topon 21526  df-bases 21561  df-cn 21842  df-hmeo 22370  df-ii 23492  df-cvm 32631 This theorem is referenced by:  cvmliftlem10  32669
 Copyright terms: Public domain W3C validator