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

Theorem cvmliftlem10 32534
 Description: Lemma for cvmlift 32539. The function 𝐾 is going to be our complete lifted path, formed by unioning together all the 𝑄 functions (each of which is defined on one segment [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] of the interval). Here we prove by induction that 𝐾 is a continuous function and a lift of 𝐺 by applying cvmliftlem6 32530, cvmliftlem7 32531 (to show it is a function and a lift), cvmliftlem8 32532 (to show it is continuous), and cvmliftlem9 32533 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 21894 gives that 𝐾 is well-defined and continuous). (Contributed by Mario Carneiro, 14-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, 𝑃⟩}⟩}))
cvmliftlem.k 𝐾 = 𝑘 ∈ (1...𝑁)(𝑄𝑘)
cvmliftlem10.1 (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
Assertion
Ref Expression
cvmliftlem10 (𝜑 → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
Distinct variable groups:   𝑣,𝑏,𝑧,𝐵   𝑗,𝑏,𝑘,𝑚,𝑛,𝑠,𝑢,𝑥,𝐹,𝑣,𝑧   𝑛,𝐿,𝑧   𝑃,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧   𝐶,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑧   𝜑,𝑗,𝑛,𝑠,𝑥,𝑧   𝑁,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧   𝑆,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧   𝑗,𝑋   𝐺,𝑏,𝑗,𝑘,𝑚,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧   𝑇,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧   𝐽,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧   𝑄,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑣,𝑢,𝑘,𝑚,𝑏)   𝜒(𝑥,𝑧,𝑣,𝑢,𝑗,𝑘,𝑚,𝑛,𝑠,𝑏)   𝐵(𝑥,𝑢,𝑗,𝑘,𝑚,𝑛,𝑠)   𝐶(𝑥,𝑚)   𝑃(𝑗,𝑠)   𝑄(𝑗,𝑠)   𝑆(𝑚)   𝑇(𝑛)   𝐽(𝑚)   𝐾(𝑥,𝑧,𝑣,𝑢,𝑗,𝑘,𝑚,𝑛,𝑠,𝑏)   𝐿(𝑥,𝑣,𝑢,𝑗,𝑘,𝑚,𝑠,𝑏)   𝑁(𝑗,𝑠)   𝑋(𝑥,𝑧,𝑣,𝑢,𝑘,𝑚,𝑛,𝑠,𝑏)

Proof of Theorem cvmliftlem10
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cvmliftlem.n . . . 4 (𝜑𝑁 ∈ ℕ)
2 nnuz 12273 . . . 4 ℕ = (ℤ‘1)
31, 2eleqtrdi 2921 . . 3 (𝜑𝑁 ∈ (ℤ‘1))
4 eluzfz2 12907 . . 3 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
53, 4syl 17 . 2 (𝜑𝑁 ∈ (1...𝑁))
6 eleq1 2898 . . . . . 6 (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7 oveq2 7156 . . . . . . . . . . 11 (𝑦 = 1 → (1...𝑦) = (1...1))
8 1z 12004 . . . . . . . . . . . 12 1 ∈ ℤ
9 fzsn 12941 . . . . . . . . . . . 12 (1 ∈ ℤ → (1...1) = {1})
108, 9ax-mp 5 . . . . . . . . . . 11 (1...1) = {1}
117, 10syl6eq 2870 . . . . . . . . . 10 (𝑦 = 1 → (1...𝑦) = {1})
1211iuneq1d 4937 . . . . . . . . 9 (𝑦 = 1 → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ {1} (𝑄𝑘))
13 1ex 10629 . . . . . . . . . 10 1 ∈ V
14 fveq2 6663 . . . . . . . . . 10 (𝑘 = 1 → (𝑄𝑘) = (𝑄‘1))
1513, 14iunxsn 5004 . . . . . . . . 9 𝑘 ∈ {1} (𝑄𝑘) = (𝑄‘1)
1612, 15syl6eq 2870 . . . . . . . 8 (𝑦 = 1 → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = (𝑄‘1))
17 oveq1 7155 . . . . . . . . . . 11 (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
1817oveq2d 7164 . . . . . . . . . 10 (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
1918oveq2d 7164 . . . . . . . . 9 (𝑦 = 1 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](1 / 𝑁))))
2019oveq1d 7163 . . . . . . . 8 (𝑦 = 1 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
2116, 20eleq12d 2905 . . . . . . 7 (𝑦 = 1 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶)))
2216coeq2d 5726 . . . . . . . 8 (𝑦 = 1 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 ∘ (𝑄‘1)))
2318reseq2d 5846 . . . . . . . 8 (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
2422, 23eqeq12d 2835 . . . . . . 7 (𝑦 = 1 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
2521, 24anbi12d 632 . . . . . 6 (𝑦 = 1 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
266, 25imbi12d 347 . . . . 5 (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))
2726imbi2d 343 . . . 4 (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))))
28 eleq1 2898 . . . . . 6 (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29 oveq2 7156 . . . . . . . . 9 (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
3029iuneq1d 4937 . . . . . . . 8 (𝑦 = 𝑛 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
31 oveq1 7155 . . . . . . . . . . 11 (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
3231oveq2d 7164 . . . . . . . . . 10 (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
3332oveq2d 7164 . . . . . . . . 9 (𝑦 = 𝑛 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
3433oveq1d 7163 . . . . . . . 8 (𝑦 = 𝑛 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
3530, 34eleq12d 2905 . . . . . . 7 (𝑦 = 𝑛 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
3630coeq2d 5726 . . . . . . . 8 (𝑦 = 𝑛 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)))
3732reseq2d 5846 . . . . . . . 8 (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
3836, 37eqeq12d 2835 . . . . . . 7 (𝑦 = 𝑛 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
3935, 38anbi12d 632 . . . . . 6 (𝑦 = 𝑛 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
4028, 39imbi12d 347 . . . . 5 (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
4140imbi2d 343 . . . 4 (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))))
42 eleq1 2898 . . . . . 6 (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43 oveq2 7156 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
4443iuneq1d 4937 . . . . . . . 8 (𝑦 = (𝑛 + 1) → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘))
45 oveq1 7155 . . . . . . . . . . 11 (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
4645oveq2d 7164 . . . . . . . . . 10 (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
4746oveq2d 7164 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
4847oveq1d 7163 . . . . . . . 8 (𝑦 = (𝑛 + 1) → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
4944, 48eleq12d 2905 . . . . . . 7 (𝑦 = (𝑛 + 1) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
5044coeq2d 5726 . . . . . . . 8 (𝑦 = (𝑛 + 1) → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)))
5146reseq2d 5846 . . . . . . . 8 (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
5250, 51eqeq12d 2835 . . . . . . 7 (𝑦 = (𝑛 + 1) → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
5349, 52anbi12d 632 . . . . . 6 (𝑦 = (𝑛 + 1) → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
5442, 53imbi12d 347 . . . . 5 (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
5554imbi2d 343 . . . 4 (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
56 eleq1 2898 . . . . . 6 (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57 oveq2 7156 . . . . . . . . . 10 (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
5857iuneq1d 4937 . . . . . . . . 9 (𝑦 = 𝑁 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...𝑁)(𝑄𝑘))
59 cvmliftlem.k . . . . . . . . 9 𝐾 = 𝑘 ∈ (1...𝑁)(𝑄𝑘)
6058, 59syl6eqr 2872 . . . . . . . 8 (𝑦 = 𝑁 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝐾)
61 oveq1 7155 . . . . . . . . . . 11 (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
6261oveq2d 7164 . . . . . . . . . 10 (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
6362oveq2d 7164 . . . . . . . . 9 (𝑦 = 𝑁 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](𝑁 / 𝑁))))
6463oveq1d 7163 . . . . . . . 8 (𝑦 = 𝑁 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶))
6560, 64eleq12d 2905 . . . . . . 7 (𝑦 = 𝑁 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
6660coeq2d 5726 . . . . . . . 8 (𝑦 = 𝑁 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹𝐾))
6762reseq2d 5846 . . . . . . . 8 (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
6866, 67eqeq12d 2835 . . . . . . 7 (𝑦 = 𝑁 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
6965, 68anbi12d 632 . . . . . 6 (𝑦 = 𝑁 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
7056, 69imbi12d 347 . . . . 5 (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
7170imbi2d 343 . . . 4 (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))))
72 eluzfz1 12906 . . . . . . . . 9 (𝑁 ∈ (ℤ‘1) → 1 ∈ (1...𝑁))
733, 72syl 17 . . . . . . . 8 (𝜑 → 1 ∈ (1...𝑁))
74 cvmliftlem.1 . . . . . . . . 9 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
75 cvmliftlem.b . . . . . . . . 9 𝐵 = 𝐶
76 cvmliftlem.x . . . . . . . . 9 𝑋 = 𝐽
77 cvmliftlem.f . . . . . . . . 9 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
78 cvmliftlem.g . . . . . . . . 9 (𝜑𝐺 ∈ (II Cn 𝐽))
79 cvmliftlem.p . . . . . . . . 9 (𝜑𝑃𝐵)
80 cvmliftlem.e . . . . . . . . 9 (𝜑 → (𝐹𝑃) = (𝐺‘0))
81 cvmliftlem.t . . . . . . . . 9 (𝜑𝑇:(1...𝑁)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)))
82 cvmliftlem.a . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇𝑘)))
83 cvmliftlem.l . . . . . . . . 9 𝐿 = (topGen‘ran (,))
84 cvmliftlem.q . . . . . . . . 9 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
85 eqid 2819 . . . . . . . . 9 (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
8674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem8 32532 . . . . . . . 8 ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
8773, 86mpdan 685 . . . . . . 7 (𝜑 → (𝑄‘1) ∈ ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88 1m1e0 11701 . . . . . . . . . . . 12 (1 − 1) = 0
8988oveq1i 7158 . . . . . . . . . . 11 ((1 − 1) / 𝑁) = (0 / 𝑁)
901nncnd 11646 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
911nnne0d 11679 . . . . . . . . . . . 12 (𝜑𝑁 ≠ 0)
9290, 91div0d 11407 . . . . . . . . . . 11 (𝜑 → (0 / 𝑁) = 0)
9389, 92syl5eq 2866 . . . . . . . . . 10 (𝜑 → ((1 − 1) / 𝑁) = 0)
9493oveq1d 7163 . . . . . . . . 9 (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
9594oveq2d 7164 . . . . . . . 8 (𝜑 → (𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿t (0[,](1 / 𝑁))))
9695oveq1d 7163 . . . . . . 7 (𝜑 → ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
9787, 96eleqtrd 2913 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
98 simpr 487 . . . . . . . . . 10 ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁))
9974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem7 32531 . . . . . . . . . 10 ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((1 − 1) / 𝑁))}))
10074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99cvmliftlem6 32530 . . . . . . . . 9 ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
10173, 100mpdan 685 . . . . . . . 8 (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
102101simprd 498 . . . . . . 7 (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))
10394reseq2d 5846 . . . . . . 7 (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104102, 103eqtrd 2854 . . . . . 6 (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))
10597, 104jca 514 . . . . 5 (𝜑 → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
106105a1d 25 . . . 4 (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
107 elnnuz 12274 . . . . . . . . 9 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
108107biimpi 218 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
109108adantl 484 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
110 peano2fzr 12912 . . . . . . . 8 ((𝑛 ∈ (ℤ‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
111110ex 415 . . . . . . 7 (𝑛 ∈ (ℤ‘1) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
112109, 111syl 17 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
113112imim1d 82 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
114 cvmliftlem10.1 . . . . . . 7 (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
115 eqid 2819 . . . . . . . . 9 (𝐿t (0[,]((𝑛 + 1) / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁)))
116 0re 10635 . . . . . . . . . . 11 0 ∈ ℝ
117114simplbi 500 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
118117adantl 484 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
119118simprd 498 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (𝑛 + 1) ∈ (1...𝑁))
120 elfznn 12928 . . . . . . . . . . . . . 14 ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121119, 120syl 17 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝑛 + 1) ∈ ℕ)
122121nnred 11645 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑛 + 1) ∈ ℝ)
1231adantr 483 . . . . . . . . . . . 12 ((𝜑𝜒) → 𝑁 ∈ ℕ)
124122, 123nndivred 11683 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125 iccssre 12810 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
126116, 124, 125sylancr 589 . . . . . . . . . 10 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
127117simpld 497 . . . . . . . . . . . . . . 15 (𝜒𝑛 ∈ ℕ)
128127adantl 484 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 𝑛 ∈ ℕ)
129128nnred 11645 . . . . . . . . . . . . 13 ((𝜑𝜒) → 𝑛 ∈ ℝ)
130129, 123nndivred 11683 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131 icccld 23367 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132116, 130, 131sylancr 589 . . . . . . . . . . 11 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
13383fveq2i 6666 . . . . . . . . . . 11 (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134132, 133eleqtrrdi 2922 . . . . . . . . . 10 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135 ssun1 4146 . . . . . . . . . . 11 (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136116a1i 11 . . . . . . . . . . . 12 ((𝜑𝜒) → 0 ∈ ℝ)
137128nnnn0d 11947 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → 𝑛 ∈ ℕ0)
138137nn0ge0d 11950 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 0 ≤ 𝑛)
139123nnred 11645 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 𝑁 ∈ ℝ)
140123nngt0d 11678 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 0 < 𝑁)
141 divge0 11501 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142129, 138, 139, 140, 141syl22anc 836 . . . . . . . . . . . . 13 ((𝜑𝜒) → 0 ≤ (𝑛 / 𝑁))
143129ltp1d 11562 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → 𝑛 < (𝑛 + 1))
144 ltdiv1 11496 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145129, 122, 139, 140, 144syl112anc 1369 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146143, 145mpbid 234 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147130, 124, 146ltled 10780 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148 elicc2 12793 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
149116, 124, 148sylancr 589 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
150130, 142, 147, 149mpbir3and 1337 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151 iccsplit 12863 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152136, 124, 150, 151syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153135, 152sseqtrrid 4018 . . . . . . . . . 10 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154 uniretop 23363 . . . . . . . . . . . 12 ℝ = (topGen‘ran (,))
15583unieqi 4839 . . . . . . . . . . . 12 𝐿 = (topGen‘ran (,))
156154, 155eqtr4i 2845 . . . . . . . . . . 11 ℝ = 𝐿
157156restcldi 21773 . . . . . . . . . 10 (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
158126, 134, 153, 157syl3anc 1366 . . . . . . . . 9 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
159 icccld 23367 . . . . . . . . . . . 12 (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160130, 124, 159syl2anc 586 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161160, 133eleqtrrdi 2922 . . . . . . . . . 10 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162 ssun2 4147 . . . . . . . . . . 11 ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163162, 152sseqtrrid 4018 . . . . . . . . . 10 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164156restcldi 21773 . . . . . . . . . 10 (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
165126, 161, 163, 164syl3anc 1366 . . . . . . . . 9 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
166 retop 23362 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Top
16783, 166eqeltri 2907 . . . . . . . . . . 11 𝐿 ∈ Top
168156restuni 21762 . . . . . . . . . . 11 ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
169167, 126, 168sylancr 589 . . . . . . . . . 10 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
170152, 169eqtr3d 2856 . . . . . . . . 9 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
171114simprbi 499 . . . . . . . . . . . . . . . 16 (𝜒 → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
172171adantl 484 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
173172simpld 497 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
174 eqid 2819 . . . . . . . . . . . . . . 15 (𝐿t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁)))
175174, 75cnf 21846 . . . . . . . . . . . . . 14 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) → 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵)
176173, 175syl 17 . . . . . . . . . . . . 13 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵)
177 iccssre 12810 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178116, 130, 177sylancr 589 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179156restuni 21762 . . . . . . . . . . . . . . 15 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = (𝐿t (0[,](𝑛 / 𝑁))))
180167, 178, 179sylancr 589 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) = (𝐿t (0[,](𝑛 / 𝑁))))
181180feq2d 6493 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵))
182176, 181mpbird 259 . . . . . . . . . . . 12 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183 eqid 2819 . . . . . . . . . . . . . . . 16 ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184 simpr 487 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁))
18574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem7 32531 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}))
18674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185cvmliftlem6 32530 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187119, 186syldan 593 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188187simpld 497 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
189128nncnd 11646 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → 𝑛 ∈ ℂ)
190 ax-1cn 10587 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
191 pncan 10884 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192189, 190, 191sylancl 588 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193192oveq1d 7163 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194193oveq1d 7163 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195194feq2d 6493 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196188, 195mpbid 234 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197176ffund 6511 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → Fun 𝑘 ∈ (1...𝑛)(𝑄𝑘))
198128, 108syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → 𝑛 ∈ (ℤ‘1))
199 eluzfz2 12907 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ (1...𝑛))
200198, 199syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → 𝑛 ∈ (1...𝑛))
201 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 → (𝑄𝑘) = (𝑄𝑛))
202201ssiun2s 4963 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑛) → (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘))
203200, 202syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘))
204 peano2rem 10945 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
205129, 204syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → (𝑛 − 1) ∈ ℝ)
206205, 123nndivred 11683 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
207206rexrd 10683 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ*)
208130rexrd 10683 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ℝ*)
209129ltm1d 11564 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → (𝑛 − 1) < 𝑛)
210 ltdiv1 11496 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
211205, 129, 139, 140, 210syl112anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
212209, 211mpbid 234 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))
213206, 130, 212ltled 10780 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
214 ubicc2 12845 . . . . . . . . . . . . . . . . . . . 20 ((((𝑛 − 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
215207, 208, 213, 214syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216198, 119, 110syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → 𝑛 ∈ (1...𝑁))
217 eqid 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
218 simpr 487 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
21974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217cvmliftlem7 32531 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
22074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219cvmliftlem6 32530 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
221216, 220syldan 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222221simpld 497 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → (𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
223222fdmd 6516 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → dom (𝑄𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
224215, 223eleqtrrd 2914 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄𝑛))
225 funssfv 6684 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∧ (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄𝑛)) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
226197, 203, 224, 225syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
227192fveq2d 6667 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄𝑛))
228227, 193fveq12d 6670 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
22974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84cvmliftlem9 32533 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
230119, 229syldan 593 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
231193fveq2d 6667 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
232230, 231eqtr3d 2856 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
233226, 228, 2323eqtr2d 2860 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234233opeq2d 4802 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
235234sneqd 4571 . . . . . . . . . . . . . 14 ((𝜑𝜒) → {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
236182ffnd 6508 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘) Fn (0[,](𝑛 / 𝑁)))
237 0xr 10680 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
238237a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → 0 ∈ ℝ*)
239 ubicc2 12845 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240238, 208, 142, 239syl3anc 1366 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241 fnressn 6913 . . . . . . . . . . . . . . 15 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩})
242236, 240, 241syl2anc 586 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩})
243196ffnd 6508 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244124rexrd 10683 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ*)
245 lbicc2 12844 . . . . . . . . . . . . . . . 16 (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246208, 244, 147, 245syl3anc 1366 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247 fnressn 6913 . . . . . . . . . . . . . . 15 (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
248243, 246, 247syl2anc 586 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
249235, 242, 2483eqtr4d 2864 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
250 df-icc 12737 . . . . . . . . . . . . . . . . 17 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
251 xrmaxle 12568 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*𝑧 ∈ ℝ*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
252 xrlemin 12569 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
253250, 251, 252ixxin 12747 . . . . . . . . . . . . . . . 16 (((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*) ∧ ((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
254238, 208, 208, 244, 253syl22anc 836 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
255142iftrued 4473 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256147iftrued 4473 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257255, 256oveq12d 7166 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258 iccid 12775 . . . . . . . . . . . . . . . 16 ((𝑛 / 𝑁) ∈ ℝ* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259208, 258syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260254, 257, 2593eqtrd 2858 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261260reseq2d 5846 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}))
262260reseq2d 5846 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
263249, 261, 2623eqtr4d 2864 . . . . . . . . . . . 12 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264 fresaun 6542 . . . . . . . . . . . 12 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
265182, 196, 263, 264syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
266 fzsuc 12946 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
267198, 266syl 17 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
268267iuneq1d 4937 . . . . . . . . . . . . 13 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) = 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘))
269 iunxun 5007 . . . . . . . . . . . . . 14 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘))
270 ovex 7181 . . . . . . . . . . . . . . . 16 (𝑛 + 1) ∈ V
271 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑘 = (𝑛 + 1) → (𝑄𝑘) = (𝑄‘(𝑛 + 1)))
272270, 271iunxsn 5004 . . . . . . . . . . . . . . 15 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘) = (𝑄‘(𝑛 + 1))
273272uneq2i 4134 . . . . . . . . . . . . . 14 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘)) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))
274269, 273eqtri 2842 . . . . . . . . . . . . 13 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))
275268, 274syl6req 2871 . . . . . . . . . . . 12 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) = 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘))
276275feq1d 6492 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
277265, 276mpbid 234 . . . . . . . . . 10 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
278170feq2d 6493 . . . . . . . . . 10 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘): (𝐿t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
279277, 278mpbid 234 . . . . . . . . 9 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘): (𝐿t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
280275reseq1d 5845 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))))
281 fresaunres1 6544 . . . . . . . . . . . 12 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
282182, 196, 263, 281syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
283280, 282eqtr3d 2856 . . . . . . . . . 10 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
284167a1i 11 . . . . . . . . . . . 12 ((𝜑𝜒) → 𝐿 ∈ Top)
285 ovex 7181 . . . . . . . . . . . . 13 (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286285a1i 11 . . . . . . . . . . . 12 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287 restabs 21765 . . . . . . . . . . . 12 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
288284, 153, 286, 287syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
289288oveq1d 7163 . . . . . . . . . 10 ((𝜑𝜒) → (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
290173, 283, 2893eltr4d 2926 . . . . . . . . 9 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))) ∈ (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶))
29174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem8 32532 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
292119, 291syldan 593 . . . . . . . . . . 11 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
293194oveq2d 7164 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294293oveq1d 7163 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
295292, 294eleqtrd 2913 . . . . . . . . . 10 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296275reseq1d 5845 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297 fresaunres2 6543 . . . . . . . . . . . 12 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
298182, 196, 263, 297syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
299296, 298eqtr3d 2856 . . . . . . . . . 10 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
300 restabs 21765 . . . . . . . . . . . 12 ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301284, 163, 286, 300syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
302301oveq1d 7163 . . . . . . . . . 10 ((𝜑𝜒) → (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
303295, 299, 3023eltr4d 2926 . . . . . . . . 9 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
304115, 75, 158, 165, 170, 279, 290, 303paste 21894 . . . . . . . 8 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
305152reseq2d 5846 . . . . . . . . 9 ((𝜑𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306172simprd 498 . . . . . . . . . . 11 ((𝜑𝜒) → (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
307187simprd 498 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308194reseq2d 5846 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309307, 308eqtrd 2854 . . . . . . . . . . 11 ((𝜑𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310306, 309uneq12d 4138 . . . . . . . . . 10 ((𝜑𝜒) → ((𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311 coundi 6093 . . . . . . . . . 10 (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
312 resundi 5860 . . . . . . . . . 10 (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313310, 311, 3123eqtr4g 2879 . . . . . . . . 9 ((𝜑𝜒) → (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314275coeq2d 5726 . . . . . . . . 9 ((𝜑𝜒) → (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)))
315305, 313, 3143eqtr2rd 2861 . . . . . . . 8 ((𝜑𝜒) → (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
316304, 315jca 514 . . . . . . 7 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
317114, 316sylan2br 596 . . . . . 6 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
318317expr 459 . . . . 5 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
319113, 318animpimp2impd 842 . . . 4 (𝑛 ∈ ℕ → ((𝜑 → (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
32027, 41, 55, 71, 106, 319nnind 11648 . . 3 (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
3211, 320mpcom 38 . 2 (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
3225, 321mpd 15 1 (𝜑 → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1082   = wceq 1531   ∈ wcel 2108  ∀wral 3136  {crab 3140  Vcvv 3493   ∖ cdif 3931   ∪ cun 3932   ∩ cin 3933   ⊆ wss 3934  ∅c0 4289  ifcif 4465  𝒫 cpw 4537  {csn 4559  ⟨cop 4565  ∪ cuni 4830  ∪ ciun 4910   class class class wbr 5057   ↦ cmpt 5137   I cid 5452   × cxp 5546  ◡ccnv 5547  dom cdm 5548  ran crn 5549   ↾ cres 5550   “ cima 5551   ∘ ccom 5552  Fun wfun 6342   Fn wfn 6343  ⟶wf 6344  ‘cfv 6348  ℩crio 7105  (class class class)co 7148   ∈ cmpo 7150  1st c1st 7679  2nd c2nd 7680  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℕcn 11630  ℤcz 11973  ℤ≥cuz 12235  (,)cioo 12730  [,]cicc 12733  ...cfz 12884  seqcseq 13361   ↾t crest 16686  topGenctg 16703  Topctop 21493  Clsdccld 21616   Cn ccn 21824  Homeochmeo 22353  IIcii 23475   CovMap ccvm 32495 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  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 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-oadd 8098  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fi 8867  df-sup 8898  df-inf 8899  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 11631  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-icc 12737  df-fz 12885  df-seq 13362  df-exp 13422  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-rest 16688  df-topgen 16709  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-top 21494  df-topon 21511  df-bases 21546  df-cld 21619  df-cn 21827  df-hmeo 22355  df-ii 23477  df-cvm 32496 This theorem is referenced by:  cvmliftlem11  32535
 Copyright terms: Public domain W3C validator