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 31504
Description: Lemma for cvmlift 31509. 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 31500, cvmliftlem7 31501 (to show it is a function and a lift), cvmliftlem8 31502 (to show it is continuous), and cvmliftlem9 31503 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 21221 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 11837 . . . 4 ℕ = (ℤ‘1)
31, 2syl6eleq 2813 . . 3 (𝜑𝑁 ∈ (ℤ‘1))
4 eluzfz2 12463 . . 3 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
53, 4syl 17 . 2 (𝜑𝑁 ∈ (1...𝑁))
6 eleq1 2791 . . . . . 6 (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7 oveq2 6773 . . . . . . . . . . 11 (𝑦 = 1 → (1...𝑦) = (1...1))
8 1z 11520 . . . . . . . . . . . 12 1 ∈ ℤ
9 fzsn 12497 . . . . . . . . . . . 12 (1 ∈ ℤ → (1...1) = {1})
108, 9ax-mp 5 . . . . . . . . . . 11 (1...1) = {1}
117, 10syl6eq 2774 . . . . . . . . . 10 (𝑦 = 1 → (1...𝑦) = {1})
1211iuneq1d 4653 . . . . . . . . 9 (𝑦 = 1 → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ {1} (𝑄𝑘))
13 1ex 10148 . . . . . . . . . 10 1 ∈ V
14 fveq2 6304 . . . . . . . . . 10 (𝑘 = 1 → (𝑄𝑘) = (𝑄‘1))
1513, 14iunxsn 4711 . . . . . . . . 9 𝑘 ∈ {1} (𝑄𝑘) = (𝑄‘1)
1612, 15syl6eq 2774 . . . . . . . 8 (𝑦 = 1 → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = (𝑄‘1))
17 oveq1 6772 . . . . . . . . . . 11 (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
1817oveq2d 6781 . . . . . . . . . 10 (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
1918oveq2d 6781 . . . . . . . . 9 (𝑦 = 1 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](1 / 𝑁))))
2019oveq1d 6780 . . . . . . . 8 (𝑦 = 1 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
2116, 20eleq12d 2797 . . . . . . 7 (𝑦 = 1 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶)))
2216coeq2d 5392 . . . . . . . 8 (𝑦 = 1 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 ∘ (𝑄‘1)))
2318reseq2d 5503 . . . . . . . 8 (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
2422, 23eqeq12d 2739 . . . . . . 7 (𝑦 = 1 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
2521, 24anbi12d 749 . . . . . 6 (𝑦 = 1 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
266, 25imbi12d 333 . . . . 5 (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))
2726imbi2d 329 . . . 4 (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))))
28 eleq1 2791 . . . . . 6 (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29 oveq2 6773 . . . . . . . . 9 (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
3029iuneq1d 4653 . . . . . . . 8 (𝑦 = 𝑛 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
31 oveq1 6772 . . . . . . . . . . 11 (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
3231oveq2d 6781 . . . . . . . . . 10 (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
3332oveq2d 6781 . . . . . . . . 9 (𝑦 = 𝑛 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
3433oveq1d 6780 . . . . . . . 8 (𝑦 = 𝑛 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
3530, 34eleq12d 2797 . . . . . . 7 (𝑦 = 𝑛 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
3630coeq2d 5392 . . . . . . . 8 (𝑦 = 𝑛 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)))
3732reseq2d 5503 . . . . . . . 8 (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
3836, 37eqeq12d 2739 . . . . . . 7 (𝑦 = 𝑛 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
3935, 38anbi12d 749 . . . . . 6 (𝑦 = 𝑛 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
4028, 39imbi12d 333 . . . . 5 (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
4140imbi2d 329 . . . 4 (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))))
42 eleq1 2791 . . . . . 6 (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43 oveq2 6773 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
4443iuneq1d 4653 . . . . . . . 8 (𝑦 = (𝑛 + 1) → 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘))
45 oveq1 6772 . . . . . . . . . . 11 (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
4645oveq2d 6781 . . . . . . . . . 10 (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
4746oveq2d 6781 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
4847oveq1d 6780 . . . . . . . 8 (𝑦 = (𝑛 + 1) → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
4944, 48eleq12d 2797 . . . . . . 7 (𝑦 = (𝑛 + 1) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
5044coeq2d 5392 . . . . . . . 8 (𝑦 = (𝑛 + 1) → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)))
5146reseq2d 5503 . . . . . . . 8 (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
5250, 51eqeq12d 2739 . . . . . . 7 (𝑦 = (𝑛 + 1) → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
5349, 52anbi12d 749 . . . . . 6 (𝑦 = (𝑛 + 1) → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
5442, 53imbi12d 333 . . . . 5 (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
5554imbi2d 329 . . . 4 (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
56 eleq1 2791 . . . . . 6 (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57 oveq2 6773 . . . . . . . . . 10 (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
5857iuneq1d 4653 . . . . . . . . 9 (𝑦 = 𝑁 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝑘 ∈ (1...𝑁)(𝑄𝑘))
59 cvmliftlem.k . . . . . . . . 9 𝐾 = 𝑘 ∈ (1...𝑁)(𝑄𝑘)
6058, 59syl6eqr 2776 . . . . . . . 8 (𝑦 = 𝑁 𝑘 ∈ (1...𝑦)(𝑄𝑘) = 𝐾)
61 oveq1 6772 . . . . . . . . . . 11 (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
6261oveq2d 6781 . . . . . . . . . 10 (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
6362oveq2d 6781 . . . . . . . . 9 (𝑦 = 𝑁 → (𝐿t (0[,](𝑦 / 𝑁))) = (𝐿t (0[,](𝑁 / 𝑁))))
6463oveq1d 6780 . . . . . . . 8 (𝑦 = 𝑁 → ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶))
6560, 64eleq12d 2797 . . . . . . 7 (𝑦 = 𝑁 → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
6660coeq2d 5392 . . . . . . . 8 (𝑦 = 𝑁 → (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐹𝐾))
6762reseq2d 5503 . . . . . . . 8 (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
6866, 67eqeq12d 2739 . . . . . . 7 (𝑦 = 𝑁 → ((𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
6965, 68anbi12d 749 . . . . . 6 (𝑦 = 𝑁 → (( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
7056, 69imbi12d 333 . . . . 5 (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
7170imbi2d 329 . . . 4 (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑦)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑦)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))))
72 eluzfz1 12462 . . . . . . . . 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 2724 . . . . . . . . 9 (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
8674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem8 31502 . . . . . . . 8 ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
8773, 86mpdan 705 . . . . . . 7 (𝜑 → (𝑄‘1) ∈ ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88 1m1e0 11202 . . . . . . . . . . . 12 (1 − 1) = 0
8988oveq1i 6775 . . . . . . . . . . 11 ((1 − 1) / 𝑁) = (0 / 𝑁)
901nncnd 11149 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
911nnne0d 11178 . . . . . . . . . . . 12 (𝜑𝑁 ≠ 0)
9290, 91div0d 10913 . . . . . . . . . . 11 (𝜑 → (0 / 𝑁) = 0)
9389, 92syl5eq 2770 . . . . . . . . . 10 (𝜑 → ((1 − 1) / 𝑁) = 0)
9493oveq1d 6780 . . . . . . . . 9 (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
9594oveq2d 6781 . . . . . . . 8 (𝜑 → (𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿t (0[,](1 / 𝑁))))
9695oveq1d 6780 . . . . . . 7 (𝜑 → ((𝐿t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
9787, 96eleqtrd 2805 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶))
98 simpr 479 . . . . . . . . . 10 ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁))
9974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem7 31501 . . . . . . . . . 10 ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((1 − 1) / 𝑁))}))
10074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99cvmliftlem6 31500 . . . . . . . . 9 ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
10173, 100mpdan 705 . . . . . . . 8 (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
102101simprd 482 . . . . . . 7 (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))
10394reseq2d 5503 . . . . . . 7 (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104102, 103eqtrd 2758 . . . . . 6 (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))
10597, 104jca 555 . . . . 5 (𝜑 → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
106105a1d 25 . . . 4 (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
107 elnnuz 11838 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
108107biimpi 206 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
109108adantl 473 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
110 peano2fzr 12468 . . . . . . . . . 10 ((𝑛 ∈ (ℤ‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
111110ex 449 . . . . . . . . 9 (𝑛 ∈ (ℤ‘1) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
112109, 111syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
113112imim1d 82 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
114 cvmliftlem10.1 . . . . . . . . . . 11 (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
115 eqid 2724 . . . . . . . . . . . . 13 (𝐿t (0[,]((𝑛 + 1) / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁)))
116 0re 10153 . . . . . . . . . . . . . . 15 0 ∈ ℝ
117114simplbi 478 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
118117adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
119118simprd 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑛 + 1) ∈ (1...𝑁))
120 elfznn 12484 . . . . . . . . . . . . . . . . . 18 ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121119, 120syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → (𝑛 + 1) ∈ ℕ)
122121nnred 11148 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (𝑛 + 1) ∈ ℝ)
1231adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → 𝑁 ∈ ℕ)
124122, 123nndivred 11182 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125 iccssre 12369 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
126116, 124, 125sylancr 698 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
127117simpld 477 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑛 ∈ ℕ)
128127adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → 𝑛 ∈ ℕ)
129128nnred 11148 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → 𝑛 ∈ ℝ)
130129, 123nndivred 11182 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131 icccld 22692 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132116, 130, 131sylancr 698 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
13383fveq2i 6307 . . . . . . . . . . . . . . 15 (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134132, 133syl6eleqr 2814 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135 ssun1 3884 . . . . . . . . . . . . . . 15 (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136116a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → 0 ∈ ℝ)
137128nnnn0d 11464 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → 𝑛 ∈ ℕ0)
138137nn0ge0d 11467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → 0 ≤ 𝑛)
139123nnred 11148 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → 𝑁 ∈ ℝ)
140123nngt0d 11177 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → 0 < 𝑁)
141 divge0 11005 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142129, 138, 139, 140, 141syl22anc 1440 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → 0 ≤ (𝑛 / 𝑁))
143129ltp1d 11067 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → 𝑛 < (𝑛 + 1))
144 ltdiv1 11000 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145129, 122, 139, 140, 144syl112anc 1443 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146143, 145mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147130, 124, 146ltled 10298 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148 elicc2 12352 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
149116, 124, 148sylancr 698 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
150130, 142, 147, 149mpbir3and 1382 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151 iccsplit 12419 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152136, 124, 150, 151syl3anc 1439 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153135, 152syl5sseqr 3760 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154 uniretop 22688 . . . . . . . . . . . . . . . 16 ℝ = (topGen‘ran (,))
15583unieqi 4553 . . . . . . . . . . . . . . . 16 𝐿 = (topGen‘ran (,))
156154, 155eqtr4i 2749 . . . . . . . . . . . . . . 15 ℝ = 𝐿
157156restcldi 21100 . . . . . . . . . . . . . 14 (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
158126, 134, 153, 157syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
159 icccld 22692 . . . . . . . . . . . . . . . 16 (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160130, 124, 159syl2anc 696 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161160, 133syl6eleqr 2814 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162 ssun2 3885 . . . . . . . . . . . . . . 15 ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163162, 152syl5sseqr 3760 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164156restcldi 21100 . . . . . . . . . . . . . 14 (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
165126, 161, 163, 164syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿t (0[,]((𝑛 + 1) / 𝑁)))))
166 retop 22687 . . . . . . . . . . . . . . . 16 (topGen‘ran (,)) ∈ Top
16783, 166eqeltri 2799 . . . . . . . . . . . . . . 15 𝐿 ∈ Top
168156restuni 21089 . . . . . . . . . . . . . . 15 ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
169167, 126, 168sylancr 698 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
170152, 169eqtr3d 2760 . . . . . . . . . . . . 13 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t (0[,]((𝑛 + 1) / 𝑁))))
171114simprbi 483 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
172171adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
173172simpld 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
174 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝐿t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁)))
175174, 75cnf 21173 . . . . . . . . . . . . . . . . . 18 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) → 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵)
176173, 175syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵)
177 iccssre 12369 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178116, 130, 177sylancr 698 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179156restuni 21089 . . . . . . . . . . . . . . . . . . 19 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = (𝐿t (0[,](𝑛 / 𝑁))))
180167, 178, 179sylancr 698 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (0[,](𝑛 / 𝑁)) = (𝐿t (0[,](𝑛 / 𝑁))))
181180feq2d 6144 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 𝑘 ∈ (1...𝑛)(𝑄𝑘): (𝐿t (0[,](𝑛 / 𝑁)))⟶𝐵))
182176, 181mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183 eqid 2724 . . . . . . . . . . . . . . . . . . . 20 ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁))
18574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem7 31501 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}))
18674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185cvmliftlem6 31500 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187119, 186syldan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188187simpld 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
189128nncnd 11149 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → 𝑛 ∈ ℂ)
190 ax-1cn 10107 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
191 pncan 10400 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192189, 190, 191sylancl 697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193192oveq1d 6780 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194193oveq1d 6780 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195194feq2d 6144 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196188, 195mpbid 222 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197 ffun 6161 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 → Fun 𝑘 ∈ (1...𝑛)(𝑄𝑘))
198182, 197syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → Fun 𝑘 ∈ (1...𝑛)(𝑄𝑘))
199128, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝜒) → 𝑛 ∈ (ℤ‘1))
200 eluzfz2 12463 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ (1...𝑛))
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝜒) → 𝑛 ∈ (1...𝑛))
202 fveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑛 → (𝑄𝑘) = (𝑄𝑛))
203202ssiun2s 4672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑛) → (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘))
204201, 203syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘))
205 peano2rem 10461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
206129, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝜒) → (𝑛 − 1) ∈ ℝ)
207206, 123nndivred 11182 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
208207rexrd 10202 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ*)
209130rexrd 10202 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ℝ*)
210129ltm1d 11069 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝜒) → (𝑛 − 1) < 𝑛)
211 ltdiv1 11000 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
212206, 129, 139, 140, 211syl112anc 1443 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
213210, 212mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))
214207, 130, 213ltled 10298 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
215 ubicc2 12403 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑛 − 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216208, 209, 214, 215syl3anc 1439 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
217199, 119, 110syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝜒) → 𝑛 ∈ (1...𝑁))
218 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
219 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
22074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218cvmliftlem7 31501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
22174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218, 219, 220cvmliftlem6 31500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222217, 221syldan 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝜒) → ((𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
223222simpld 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝜒) → (𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
224 fdm 6164 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 → dom (𝑄𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
225223, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝜒) → dom (𝑄𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
226216, 225eleqtrrd 2806 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄𝑛))
227 funssfv 6322 . . . . . . . . . . . . . . . . . . . . . 22 ((Fun 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∧ (𝑄𝑛) ⊆ 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄𝑛)) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
228198, 204, 226, 227syl3anc 1439 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
229192fveq2d 6308 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄𝑛))
230229, 193fveq12d 6310 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
23174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84cvmliftlem9 31503 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
232119, 231syldan 488 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
233193fveq2d 6308 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234232, 233eqtr3d 2760 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
235228, 230, 2343eqtr2d 2764 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
236235opeq2d 4516 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → ⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
237236sneqd 4297 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
238 ffn 6158 . . . . . . . . . . . . . . . . . . . 20 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 𝑘 ∈ (1...𝑛)(𝑄𝑘) Fn (0[,](𝑛 / 𝑁)))
239182, 238syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → 𝑘 ∈ (1...𝑛)(𝑄𝑘) Fn (0[,](𝑛 / 𝑁)))
240 0xr 10199 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℝ*
241240a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → 0 ∈ ℝ*)
242 ubicc2 12403 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
243241, 209, 142, 242syl3anc 1439 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
244 fnressn 6540 . . . . . . . . . . . . . . . . . . 19 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩})
245239, 243, 244syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ( 𝑘 ∈ (1...𝑛)(𝑄𝑘)‘(𝑛 / 𝑁))⟩})
246 ffn 6158 . . . . . . . . . . . . . . . . . . . 20 ((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247196, 246syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
248124rexrd 10202 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ*)
249 lbicc2 12402 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
250209, 248, 147, 249syl3anc 1439 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
251 fnressn 6540 . . . . . . . . . . . . . . . . . . 19 (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
252247, 250, 251syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
253237, 245, 2523eqtr4d 2768 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
254 df-icc 12296 . . . . . . . . . . . . . . . . . . . . 21 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
255 xrmaxle 12128 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*𝑧 ∈ ℝ*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
256 xrlemin 12129 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
257254, 255, 256ixxin 12306 . . . . . . . . . . . . . . . . . . . 20 (((0 ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*) ∧ ((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
258241, 209, 209, 248, 257syl22anc 1440 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
259142iftrued 4202 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
260147iftrued 4202 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
261259, 260oveq12d 6783 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
262 iccid 12334 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 / 𝑁) ∈ ℝ* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
263209, 262syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
264258, 261, 2633eqtrd 2762 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
265264reseq2d 5503 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ {(𝑛 / 𝑁)}))
266264reseq2d 5503 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
267253, 265, 2663eqtr4d 2768 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
268 fresaun 6188 . . . . . . . . . . . . . . . 16 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
269182, 196, 267, 268syl3anc 1439 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
270 fzsuc 12502 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
271199, 270syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
272271iuneq1d 4653 . . . . . . . . . . . . . . . . 17 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) = 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘))
273 iunxun 4713 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘))
274 ovex 6793 . . . . . . . . . . . . . . . . . . . 20 (𝑛 + 1) ∈ V
275 fveq2 6304 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = (𝑛 + 1) → (𝑄𝑘) = (𝑄‘(𝑛 + 1)))
276274, 275iunxsn 4711 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘) = (𝑄‘(𝑛 + 1))
277276uneq2i 3872 . . . . . . . . . . . . . . . . . 18 ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄𝑘)) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))
278273, 277eqtri 2746 . . . . . . . . . . . . . . . . 17 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄𝑘) = ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))
279272, 278syl6req 2775 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) = 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘))
280279feq1d 6143 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
281269, 280mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
282170feq2d 6144 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘): (𝐿t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
283281, 282mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘): (𝐿t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
284279reseq1d 5502 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))))
285 fresaunres1 6190 . . . . . . . . . . . . . . . 16 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
286182, 196, 267, 285syl3anc 1439 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
287284, 286eqtr3d 2760 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))) = 𝑘 ∈ (1...𝑛)(𝑄𝑘))
288167a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → 𝐿 ∈ Top)
289 ovex 6793 . . . . . . . . . . . . . . . . 17 (0[,]((𝑛 + 1) / 𝑁)) ∈ V
290289a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
291 restabs 21092 . . . . . . . . . . . . . . . 16 ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
292288, 153, 290, 291syl3anc 1439 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿t (0[,](𝑛 / 𝑁))))
293292oveq1d 6780 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶))
294173, 287, 2933eltr4d 2818 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ (0[,](𝑛 / 𝑁))) ∈ (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶))
29574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem8 31502 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296119, 295syldan 488 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
297194oveq2d 6781 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
298297oveq1d 6780 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((𝐿t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
299296, 298eleqtrd 2805 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
300279reseq1d 5502 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301 fresaunres2 6189 . . . . . . . . . . . . . . . 16 (( 𝑘 ∈ (1...𝑛)(𝑄𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
302182, 196, 267, 301syl3anc 1439 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
303300, 302eqtr3d 2760 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
304 restabs 21092 . . . . . . . . . . . . . . . 16 ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
305288, 163, 290, 304syl3anc 1439 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
306305oveq1d 6780 . . . . . . . . . . . . . 14 ((𝜑𝜒) → (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
307299, 303, 3063eltr4d 2818 . . . . . . . . . . . . 13 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
308115, 75, 158, 165, 170, 283, 294, 307paste 21221 . . . . . . . . . . . 12 ((𝜑𝜒) → 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
309152reseq2d 5503 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
310172simprd 482 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
311187simprd 482 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
312194reseq2d 5503 . . . . . . . . . . . . . . . 16 ((𝜑𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313311, 312eqtrd 2758 . . . . . . . . . . . . . . 15 ((𝜑𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
314310, 313uneq12d 3876 . . . . . . . . . . . . . 14 ((𝜑𝜒) → ((𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
315 coundi 5749 . . . . . . . . . . . . . 14 (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
316 resundi 5520 . . . . . . . . . . . . . 14 (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
317314, 315, 3163eqtr4g 2783 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
318279coeq2d 5392 . . . . . . . . . . . . 13 ((𝜑𝜒) → (𝐹 ∘ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)))
319309, 317, 3183eqtr2rd 2765 . . . . . . . . . . . 12 ((𝜑𝜒) → (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
320308, 319jca 555 . . . . . . . . . . 11 ((𝜑𝜒) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
321114, 320sylan2br 494 . . . . . . . . . 10 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
322321expr 644 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
323322expr 644 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((𝑛 + 1) ∈ (1...𝑁) → (( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
324323a2d 29 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
325113, 324syld 47 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
326325expcom 450 . . . . 5 (𝑛 ∈ ℕ → (𝜑 → ((𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
327326a2d 29 . . . 4 (𝑛 ∈ ℕ → ((𝜑 → (𝑛 ∈ (1...𝑁) → ( 𝑘 ∈ (1...𝑛)(𝑄𝑘) ∈ ((𝐿t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...𝑛)(𝑄𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → ( 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘) ∈ ((𝐿t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 𝑘 ∈ (1...(𝑛 + 1))(𝑄𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
32827, 41, 55, 71, 106, 327nnind 11151 . . 3 (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
3291, 328mpcom 38 . 2 (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
3305, 329mpd 15 1 (𝜑 → (𝐾 ∈ ((𝐿t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wcel 2103  wral 3014  {crab 3018  Vcvv 3304  cdif 3677  cun 3678  cin 3679  wss 3680  c0 4023  ifcif 4194  𝒫 cpw 4266  {csn 4285  cop 4291   cuni 4544   ciun 4628   class class class wbr 4760  cmpt 4837   I cid 5127   × cxp 5216  ccnv 5217  dom cdm 5218  ran crn 5219  cres 5220  cima 5221  ccom 5222  Fun wfun 5995   Fn wfn 5996  wf 5997  cfv 6001  crio 6725  (class class class)co 6765  cmpt2 6767  1st c1st 7283  2nd c2nd 7284  cc 10047  cr 10048  0cc0 10049  1c1 10050   + caddc 10052  *cxr 10186   < clt 10187  cle 10188  cmin 10379   / cdiv 10797  cn 11133  cz 11490  cuz 11800  (,)cioo 12289  [,]cicc 12292  ...cfz 12440  seqcseq 12916  t crest 16204  topGenctg 16221  Topctop 20821  Clsdccld 20943   Cn ccn 21151  Homeochmeo 21679  IIcii 22800   CovMap ccvm 31465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-iin 4631  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-oadd 7684  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-fi 8433  df-sup 8464  df-inf 8465  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-n0 11406  df-z 11491  df-uz 11801  df-q 11903  df-rp 11947  df-xneg 12060  df-xadd 12061  df-xmul 12062  df-ioo 12293  df-icc 12296  df-fz 12441  df-seq 12917  df-exp 12976  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-rest 16206  df-topgen 16227  df-psmet 19861  df-xmet 19862  df-met 19863  df-bl 19864  df-mopn 19865  df-top 20822  df-topon 20839  df-bases 20873  df-cld 20946  df-cn 21154  df-hmeo 21681  df-ii 22802  df-cvm 31466
This theorem is referenced by:  cvmliftlem11  31505
  Copyright terms: Public domain W3C validator