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

Theorem cvmliftlem10 31747
Description: Lemma for cvmlift 31752. 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 31743, cvmliftlem7 31744 (to show it is a function and a lift), cvmliftlem8 31745 (to show it is continuous), and cvmliftlem9 31746 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 21394 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 11930 . . . 4 ℕ = (ℤ‘1)
31, 2syl6eleq 2854 . . 3 (𝜑𝑁 ∈ (ℤ‘1))
4 eluzfz2 12563 . . 3 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
53, 4syl 17 . 2 (𝜑𝑁 ∈ (1...𝑁))
6 eleq1 2832 . . . . . 6 (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7 oveq2 6854 . . . . . . . . . . 11 (𝑦 = 1 → (1...𝑦) = (1...1))
8 1z 11660 . . . . . . . . . . . 12 1 ∈ ℤ
9 fzsn 12597 . . . . . . . . . . . 12 (1 ∈ ℤ → (1...1) = {1})
108, 9ax-mp 5 . . . . . . . . . . 11 (1...1) = {1}
117, 10syl6eq 2815 . . . . . . . . . 10 (𝑦 = 1 → (1...𝑦) = {1})
1211iuneq1d 4703 . . . . . . . . 9 (𝑦 = 1 → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ {1} (𝑄𝑘))
13 1ex 10293 . . . . . . . . . 10 1 ∈ V
14 fveq2 6379 . . . . . . . . . 10 (𝑘 = 1 → (𝑄𝑘) = (𝑄‘1))
1513, 14iunxsn 4761 . . . . . . . . 9 𝑘 ∈ {1} (𝑄𝑘) = (𝑄‘1)
1612, 15syl6eq 2815 . . . . . . . 8 (𝑦 = 1 → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = (𝑄‘1))
17 oveq1 6853 . . . . . . . . . . 11 (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
1817oveq2d 6862 . . . . . . . . . 10 (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
1918oveq2d 6862 . . . . . . . . 9 (𝑦 = 1 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](1 / 𝑁))))
2019oveq1d 6861 . . . . . . . 8 (𝑦 = 1 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
2116, 20eleq12d 2838 . . . . . . 7 (𝑦 = 1 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶)))
2216coeq2d 5455 . . . . . . . 8 (𝑦 = 1 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 ∘ (𝑄‘1)))
2318reseq2d 5567 . . . . . . . 8 (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
2422, 23eqeq12d 2780 . . . . . . 7 (𝑦 = 1 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
2521, 24anbi12d 624 . . . . . 6 (𝑦 = 1 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
266, 25imbi12d 335 . . . . 5 (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))
2726imbi2d 331 . . . 4 (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))))
28 eleq1 2832 . . . . . 6 (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29 oveq2 6854 . . . . . . . . 9 (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
3029iuneq1d 4703 . . . . . . . 8 (𝑦 = 𝑛 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
31 oveq1 6853 . . . . . . . . . . 11 (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
3231oveq2d 6862 . . . . . . . . . 10 (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
3332oveq2d 6862 . . . . . . . . 9 (𝑦 = 𝑛 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
3433oveq1d 6861 . . . . . . . 8 (𝑦 = 𝑛 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
3530, 34eleq12d 2838 . . . . . . 7 (𝑦 = 𝑛 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
3630coeq2d 5455 . . . . . . . 8 (𝑦 = 𝑛 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)))
3732reseq2d 5567 . . . . . . . 8 (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
3836, 37eqeq12d 2780 . . . . . . 7 (𝑦 = 𝑛 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
3935, 38anbi12d 624 . . . . . 6 (𝑦 = 𝑛 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
4028, 39imbi12d 335 . . . . 5 (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
4140imbi2d 331 . . . 4 (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))))
42 eleq1 2832 . . . . . 6 (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43 oveq2 6854 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
4443iuneq1d 4703 . . . . . . . 8 (𝑦 = (𝑛 + 1) → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘))
45 oveq1 6853 . . . . . . . . . . 11 (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
4645oveq2d 6862 . . . . . . . . . 10 (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
4746oveq2d 6862 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
4847oveq1d 6861 . . . . . . . 8 (𝑦 = (𝑛 + 1) → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
4944, 48eleq12d 2838 . . . . . . 7 (𝑦 = (𝑛 + 1) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
5044coeq2d 5455 . . . . . . . 8 (𝑦 = (𝑛 + 1) → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)))
5146reseq2d 5567 . . . . . . . 8 (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
5250, 51eqeq12d 2780 . . . . . . 7 (𝑦 = (𝑛 + 1) → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
5349, 52anbi12d 624 . . . . . 6 (𝑦 = (𝑛 + 1) → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
5442, 53imbi12d 335 . . . . 5 (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
5554imbi2d 331 . . . 4 (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
56 eleq1 2832 . . . . . 6 (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57 oveq2 6854 . . . . . . . . . 10 (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
5857iuneq1d 4703 . . . . . . . . 9 (𝑦 = 𝑁 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...𝑁)(𝑄𝑘))
59 cvmliftlem.k . . . . . . . . 9 𝐾 = 𝑘 ∈ (1...𝑁)(𝑄𝑘)
6058, 59syl6eqr 2817 . . . . . . . 8 (𝑦 = 𝑁 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝐾)
61 oveq1 6853 . . . . . . . . . . 11 (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
6261oveq2d 6862 . . . . . . . . . 10 (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
6362oveq2d 6862 . . . . . . . . 9 (𝑦 = 𝑁 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](𝑁 / 𝑁))))
6463oveq1d 6861 . . . . . . . 8 (𝑦 = 𝑁 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶))
6560, 64eleq12d 2838 . . . . . . 7 (𝑦 = 𝑁 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
6660coeq2d 5455 . . . . . . . 8 (𝑦 = 𝑁 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹𝐾))
6762reseq2d 5567 . . . . . . . 8 (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
6866, 67eqeq12d 2780 . . . . . . 7 (𝑦 = 𝑁 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
6965, 68anbi12d 624 . . . . . 6 (𝑦 = 𝑁 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
7056, 69imbi12d 335 . . . . 5 (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
7170imbi2d 331 . . . 4 (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))))
72 eluzfz1 12562 . . . . . . . . 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 2765 . . . . . . . . 9 (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
8674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem8 31745 . . . . . . . 8 ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
8773, 86mpdan 678 . . . . . . 7 (𝜑 → (𝑄‘1) ∈ ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88 1m1e0 11349 . . . . . . . . . . . 12 (1 − 1) = 0
8988oveq1i 6856 . . . . . . . . . . 11 ((1 − 1) / 𝑁) = (0 / 𝑁)
901nncnd 11297 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
911nnne0d 11327 . . . . . . . . . . . 12 (𝜑𝑁 ≠ 0)
9290, 91div0d 11059 . . . . . . . . . . 11 (𝜑 → (0 / 𝑁) = 0)
9389, 92syl5eq 2811 . . . . . . . . . 10 (𝜑 → ((1 − 1) / 𝑁) = 0)
9493oveq1d 6861 . . . . . . . . 9 (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
9594oveq2d 6862 . . . . . . . 8 (𝜑 → (𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿t (0[,](1 / 𝑁))))
9695oveq1d 6861 . . . . . . 7 (𝜑 → ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
9787, 96eleqtrd 2846 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
98 simpr 477 . . . . . . . . . 10 ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁))
9974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem7 31744 . . . . . . . . . 10 ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((1 − 1) / 𝑁))}))
10074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99cvmliftlem6 31743 . . . . . . . . 9 ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
10173, 100mpdan 678 . . . . . . . 8 (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
102101simprd 489 . . . . . . 7 (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))
10394reseq2d 5567 . . . . . . 7 (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104102, 103eqtrd 2799 . . . . . 6 (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))
10597, 104jca 507 . . . . 5 (𝜑 → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
106105a1d 25 . . . 4 (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
107 elnnuz 11931 . . . . . . . . 9 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
108107biimpi 207 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
109108adantl 473 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
110 peano2fzr 12568 . . . . . . . 8 ((𝑛 ∈ (ℤ‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
111110ex 401 . . . . . . 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 2765 . . . . . . . . 9 (𝐿t (0[,]((𝑛 + 1) / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁)))
116 0re 10299 . . . . . . . . . . 11 0 ∈ ℝ
117114simplbi 491 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
118117adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
119118simprd 489 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (𝑛 + 1) ∈ (1...𝑁))
120 elfznn 12584 . . . . . . . . . . . . . 14 ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121119, 120syl 17 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝑛 + 1) ∈ ℕ)
122121nnred 11296 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑛 + 1) ∈ ℝ)
1231adantr 472 . . . . . . . . . . . 12 ((𝜑𝜒) → 𝑁 ∈ ℕ)
124122, 123nndivred 11331 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125 iccssre 12464 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
126116, 124, 125sylancr 581 . . . . . . . . . 10 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
127117simpld 488 . . . . . . . . . . . . . . 15 (𝜒𝑛 ∈ ℕ)
128127adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 𝑛 ∈ ℕ)
129128nnred 11296 . . . . . . . . . . . . 13 ((𝜑𝜒) → 𝑛 ∈ ℝ)
130129, 123nndivred 11331 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131 icccld 22865 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132116, 130, 131sylancr 581 . . . . . . . . . . 11 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
13383fveq2i 6382 . . . . . . . . . . 11 (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134132, 133syl6eleqr 2855 . . . . . . . . . 10 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135 ssun1 3940 . . . . . . . . . . 11 (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136116a1i 11 . . . . . . . . . . . 12 ((𝜑𝜒) → 0 ∈ ℝ)
137128nnnn0d 11603 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → 𝑛 ∈ ℕ0)
138137nn0ge0d 11606 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 0 ≤ 𝑛)
139123nnred 11296 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 𝑁 ∈ ℝ)
140123nngt0d 11326 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 0 < 𝑁)
141 divge0 11151 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142129, 138, 139, 140, 141syl22anc 867 . . . . . . . . . . . . 13 ((𝜑𝜒) → 0 ≤ (𝑛 / 𝑁))
143129ltp1d 11213 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → 𝑛 < (𝑛 + 1))
144 ltdiv1 11146 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145129, 122, 139, 140, 144syl112anc 1493 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146143, 145mpbid 223 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147130, 124, 146ltled 10444 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148 elicc2 12447 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
149116, 124, 148sylancr 581 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
150130, 142, 147, 149mpbir3and 1442 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151 iccsplit 12519 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152136, 124, 150, 151syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153135, 152syl5sseqr 3816 . . . . . . . . . 10 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154 uniretop 22861 . . . . . . . . . . . 12 ℝ = (topGen‘ran (,))
15583unieqi 4605 . . . . . . . . . . . 12 𝐿 = (topGen‘ran (,))
156154, 155eqtr4i 2790 . . . . . . . . . . 11 ℝ = 𝐿
157156restcldi 21273 . . . . . . . . . 10 (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
158126, 134, 153, 157syl3anc 1490 . . . . . . . . 9 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
159 icccld 22865 . . . . . . . . . . . 12 (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160130, 124, 159syl2anc 579 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161160, 133syl6eleqr 2855 . . . . . . . . . 10 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162 ssun2 3941 . . . . . . . . . . 11 ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163162, 152syl5sseqr 3816 . . . . . . . . . 10 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164156restcldi 21273 . . . . . . . . . 10 (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
165126, 161, 163, 164syl3anc 1490 . . . . . . . . 9 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
166 retop 22860 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Top
16783, 166eqeltri 2840 . . . . . . . . . . 11 𝐿 ∈ Top
168156restuni 21262 . . . . . . . . . . 11 ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
169167, 126, 168sylancr 581 . . . . . . . . . 10 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
170152, 169eqtr3d 2801 . . . . . . . . 9 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
171114simprbi 490 . . . . . . . . . . . . . . . 16 (𝜒 → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
172171adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
173172simpld 488 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
174 eqid 2765 . . . . . . . . . . . . . . 15 (𝐿t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁)))
175174, 75cnf 21346 . . . . . . . . . . . . . 14 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) → 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵)
176173, 175syl 17 . . . . . . . . . . . . 13 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵)
177 iccssre 12464 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178116, 130, 177sylancr 581 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179156restuni 21262 . . . . . . . . . . . . . . 15 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = (𝐿t (0[,](𝑛 / 𝑁))))
180167, 178, 179sylancr 581 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) = (𝐿t (0[,](𝑛 / 𝑁))))
181180feq2d 6211 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵))
182176, 181mpbird 248 . . . . . . . . . . . 12 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183 eqid 2765 . . . . . . . . . . . . . . . 16 ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁))
18574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem7 31744 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}))
18674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185cvmliftlem6 31743 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187119, 186syldan 585 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188187simpld 488 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
189128nncnd 11297 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → 𝑛 ∈ ℂ)
190 ax-1cn 10251 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
191 pncan 10546 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192189, 190, 191sylancl 580 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193192oveq1d 6861 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194193oveq1d 6861 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195194feq2d 6211 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196188, 195mpbid 223 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197176ffund 6229 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → Fun 𝑘 ∈ (1...𝑛)(𝑄𝑘))
198128, 108syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → 𝑛 ∈ (ℤ‘1))
199 eluzfz2 12563 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ (1...𝑛))
200198, 199syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → 𝑛 ∈ (1...𝑛))
201 fveq2 6379 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑛 → (𝑄𝑘) = (𝑄𝑛))
202201ssiun2s 4722 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑛) → (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘))
203200, 202syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘))
204 peano2rem 10607 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
205129, 204syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → (𝑛 − 1) ∈ ℝ)
206205, 123nndivred 11331 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
207206rexrd 10347 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ*)
208130rexrd 10347 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ℝ*)
209129ltm1d 11215 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → (𝑛 − 1) < 𝑛)
210 ltdiv1 11146 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
211205, 129, 139, 140, 210syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
212209, 211mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))
213206, 130, 212ltled 10444 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
214 ubicc2 12500 . . . . . . . . . . . . . . . . . . . 20 ((((𝑛 − 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
215207, 208, 213, 214syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216198, 119, 110syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → 𝑛 ∈ (1...𝑁))
217 eqid 2765 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
218 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
21974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217cvmliftlem7 31744 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
22074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219cvmliftlem6 31743 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
221216, 220syldan 585 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222221simpld 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → (𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
223222fdmd 6234 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → dom (𝑄𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
224215, 223eleqtrrd 2847 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄𝑛))
225 funssfv 6400 . . . . . . . . . . . . . . . . . 18 ((Fun 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∧ (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄𝑛)) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
226197, 203, 224, 225syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
227192fveq2d 6383 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄𝑛))
228227, 193fveq12d 6386 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
22974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84cvmliftlem9 31746 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
230119, 229syldan 585 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
231193fveq2d 6383 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
232230, 231eqtr3d 2801 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
233226, 228, 2323eqtr2d 2805 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234233opeq2d 4568 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
235234sneqd 4348 . . . . . . . . . . . . . 14 ((𝜑𝜒) → {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
236182ffnd 6226 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘) Fn (0[,](𝑛 / 𝑁)))
237 0xr 10344 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
238237a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → 0 ∈ ℝ*)
239 ubicc2 12500 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240238, 208, 142, 239syl3anc 1490 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241 fnressn 6621 . . . . . . . . . . . . . . 15 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩})
242236, 240, 241syl2anc 579 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩})
243196ffnd 6226 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244124rexrd 10347 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ*)
245 lbicc2 12499 . . . . . . . . . . . . . . . 16 (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246208, 244, 147, 245syl3anc 1490 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247 fnressn 6621 . . . . . . . . . . . . . . 15 (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
248243, 246, 247syl2anc 579 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
249235, 242, 2483eqtr4d 2809 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
250 df-icc 12391 . . . . . . . . . . . . . . . . 17 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
251 xrmaxle 12223 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*𝑧 ∈ ℝ*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
252 xrlemin 12224 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
253250, 251, 252ixxin 12401 . . . . . . . . . . . . . . . 16 (((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*) ∧ ((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
254238, 208, 208, 244, 253syl22anc 867 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
255142iftrued 4253 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256147iftrued 4253 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257255, 256oveq12d 6864 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258 iccid 12429 . . . . . . . . . . . . . . . 16 ((𝑛 / 𝑁) ∈ ℝ* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259208, 258syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260254, 257, 2593eqtrd 2803 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261260reseq2d 5567 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}))
262260reseq2d 5567 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
263249, 261, 2623eqtr4d 2809 . . . . . . . . . . . 12 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264 fresaun 6259 . . . . . . . . . . . 12 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
265182, 196, 263, 264syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
266 fzsuc 12602 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
267198, 266syl 17 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
268267iuneq1d 4703 . . . . . . . . . . . . 13 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) = 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘))
269 iunxun 4764 . . . . . . . . . . . . . 14 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘))
270 ovex 6878 . . . . . . . . . . . . . . . 16 (𝑛 + 1) ∈ V
271 fveq2 6379 . . . . . . . . . . . . . . . 16 (𝑘 = (𝑛 + 1) → (𝑄𝑘) = (𝑄‘(𝑛 + 1)))
272270, 271iunxsn 4761 . . . . . . . . . . . . . . 15 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘) = (𝑄‘(𝑛 + 1))
273272uneq2i 3928 . . . . . . . . . . . . . 14 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘)) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))
274269, 273eqtri 2787 . . . . . . . . . . . . 13 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))
275268, 274syl6req 2816 . . . . . . . . . . . 12 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) = 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘))
276275feq1d 6210 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
277265, 276mpbid 223 . . . . . . . . . 10 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
278170feq2d 6211 . . . . . . . . . 10 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘): (𝐿t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
279277, 278mpbid 223 . . . . . . . . 9 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘): (𝐿t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
280275reseq1d 5566 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))))
281 fresaunres1 6261 . . . . . . . . . . . 12 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
282182, 196, 263, 281syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
283280, 282eqtr3d 2801 . . . . . . . . . 10 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
284167a1i 11 . . . . . . . . . . . 12 ((𝜑𝜒) → 𝐿 ∈ Top)
285 ovex 6878 . . . . . . . . . . . . 13 (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286285a1i 11 . . . . . . . . . . . 12 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287 restabs 21265 . . . . . . . . . . . 12 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
288284, 153, 286, 287syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
289288oveq1d 6861 . . . . . . . . . 10 ((𝜑𝜒) → (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
290173, 283, 2893eltr4d 2859 . . . . . . . . 9 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))) ∈ (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶))
29174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem8 31745 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
292119, 291syldan 585 . . . . . . . . . . 11 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
293194oveq2d 6862 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294293oveq1d 6861 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
295292, 294eleqtrd 2846 . . . . . . . . . 10 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296275reseq1d 5566 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297 fresaunres2 6260 . . . . . . . . . . . 12 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
298182, 196, 263, 297syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
299296, 298eqtr3d 2801 . . . . . . . . . 10 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
300 restabs 21265 . . . . . . . . . . . 12 ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301284, 163, 286, 300syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝜒) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
302301oveq1d 6861 . . . . . . . . . 10 ((𝜑𝜒) → (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
303295, 299, 3023eltr4d 2859 . . . . . . . . 9 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
304115, 75, 158, 165, 170, 279, 290, 303paste 21394 . . . . . . . 8 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
305152reseq2d 5567 . . . . . . . . 9 ((𝜑𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306172simprd 489 . . . . . . . . . . 11 ((𝜑𝜒) → (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
307187simprd 489 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308194reseq2d 5567 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309307, 308eqtrd 2799 . . . . . . . . . . 11 ((𝜑𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310306, 309uneq12d 3932 . . . . . . . . . 10 ((𝜑𝜒) → ((𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311 coundi 5824 . . . . . . . . . 10 (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
312 resundi 5588 . . . . . . . . . 10 (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313310, 311, 3123eqtr4g 2824 . . . . . . . . 9 ((𝜑𝜒) → (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314275coeq2d 5455 . . . . . . . . 9 ((𝜑𝜒) → (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)))
315305, 313, 3143eqtr2rd 2806 . . . . . . . 8 ((𝜑𝜒) → (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
316304, 315jca 507 . . . . . . 7 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
317114, 316sylan2br 588 . . . . . 6 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
318317expr 448 . . . . 5 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
319113, 318animpimp2impd 872 . . . 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 11299 . . 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 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  {crab 3059  Vcvv 3350  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081  ifcif 4245  𝒫 cpw 4317  {csn 4336  cop 4342   cuni 4596   ciun 4678   class class class wbr 4811  cmpt 4890   I cid 5186   × cxp 5277  ccnv 5278  dom cdm 5279  ran crn 5280  cres 5281  cima 5282  ccom 5283  Fun wfun 6064   Fn wfn 6065  wf 6066  cfv 6070  crio 6806  (class class class)co 6846  cmpt2 6848  1st c1st 7368  2nd c2nd 7369  cc 10191  cr 10192  0cc0 10193  1c1 10194   + caddc 10196  *cxr 10331   < clt 10332  cle 10333  cmin 10525   / cdiv 10943  cn 11279  cz 11629  cuz 11893  (,)cioo 12384  [,]cicc 12387  ...cfz 12540  seqcseq 13015  t crest 16363  topGenctg 16380  Topctop 20993  Clsdccld 21116   Cn ccn 21324  Homeochmeo 21852  IIcii 22973   CovMap ccvm 31708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-oadd 7772  df-er 7951  df-map 8066  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fi 8528  df-sup 8559  df-inf 8560  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10527  df-neg 10528  df-div 10944  df-nn 11280  df-2 11340  df-3 11341  df-n0 11544  df-z 11630  df-uz 11894  df-q 11997  df-rp 12036  df-xneg 12153  df-xadd 12154  df-xmul 12155  df-ioo 12388  df-icc 12391  df-fz 12541  df-seq 13016  df-exp 13075  df-cj 14140  df-re 14141  df-im 14142  df-sqrt 14276  df-abs 14277  df-rest 16365  df-topgen 16386  df-psmet 20027  df-xmet 20028  df-met 20029  df-bl 20030  df-mopn 20031  df-top 20994  df-topon 21011  df-bases 21046  df-cld 21119  df-cn 21327  df-hmeo 21854  df-ii 22975  df-cvm 31709
This theorem is referenced by:  cvmliftlem11  31748
  Copyright terms: Public domain W3C validator