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

Theorem cvmliftlem7 31721
Description: Lemma for cvmlift 31729. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 31720 to show functionality and lifting of 𝑄). (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, 𝑃⟩}⟩}))
cvmliftlem5.3 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))
Assertion
Ref Expression
cvmliftlem7 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
Distinct variable groups:   𝑣,𝑏,𝑧,𝐵   𝑗,𝑏,𝑘,𝑚,𝑠,𝑢,𝑥,𝐹,𝑣,𝑧   𝑧,𝐿   𝑀,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧   𝑃,𝑏,𝑘,𝑚,𝑢,𝑣,𝑥,𝑧   𝐶,𝑏,𝑗,𝑘,𝑠,𝑢,𝑣,𝑧   𝜑,𝑗,𝑠,𝑥,𝑧   𝑁,𝑏,𝑘,𝑚,𝑢,𝑣,𝑥,𝑧   𝑆,𝑏,𝑗,𝑘,𝑠,𝑢,𝑣,𝑥,𝑧   𝑗,𝑋   𝐺,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧   𝑇,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧   𝐽,𝑏,𝑗,𝑘,𝑠,𝑢,𝑣,𝑥,𝑧   𝑄,𝑏,𝑘,𝑚,𝑢,𝑣,𝑥,𝑧   𝑘,𝑊,𝑚,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑣,𝑢,𝑘,𝑚,𝑏)   𝐵(𝑥,𝑢,𝑗,𝑘,𝑚,𝑠)   𝐶(𝑥,𝑚)   𝑃(𝑗,𝑠)   𝑄(𝑗,𝑠)   𝑆(𝑚)   𝐽(𝑚)   𝐿(𝑥,𝑣,𝑢,𝑗,𝑘,𝑚,𝑠,𝑏)   𝑁(𝑗,𝑠)   𝑊(𝑣,𝑢,𝑗,𝑠,𝑏)   𝑋(𝑥,𝑧,𝑣,𝑢,𝑘,𝑚,𝑠,𝑏)

Proof of Theorem cvmliftlem7
Dummy variables 𝑦 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzssp1 12591 . . . 4 (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
2 cvmliftlem.n . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
32nncnd 11292 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
43adantr 472 . . . . . 6 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
5 ax-1cn 10247 . . . . . 6 1 ∈ ℂ
6 npcan 10544 . . . . . 6 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
74, 5, 6sylancl 580 . . . . 5 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑁 − 1) + 1) = 𝑁)
87oveq2d 6858 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → (0...((𝑁 − 1) + 1)) = (0...𝑁))
91, 8syl5sseq 3813 . . 3 ((𝜑𝑀 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
10 simpr 477 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
11 elfzelz 12549 . . . . 5 (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℤ)
122nnzd 11728 . . . . 5 (𝜑𝑁 ∈ ℤ)
13 elfzm1b 12625 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
1411, 12, 13syl2anr 590 . . . 4 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
1510, 14mpbid 223 . . 3 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
169, 15sseldd 3762 . 2 ((𝜑𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...𝑁))
17 elfznn0 12640 . . . 4 ((𝑀 − 1) ∈ (0...𝑁) → (𝑀 − 1) ∈ ℕ0)
1817adantl 473 . . 3 ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → (𝑀 − 1) ∈ ℕ0)
19 eleq1 2832 . . . . . . 7 (𝑦 = 0 → (𝑦 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
20 fveq2 6375 . . . . . . . . 9 (𝑦 = 0 → (𝑄𝑦) = (𝑄‘0))
21 oveq1 6849 . . . . . . . . 9 (𝑦 = 0 → (𝑦 / 𝑁) = (0 / 𝑁))
2220, 21fveq12d 6382 . . . . . . . 8 (𝑦 = 0 → ((𝑄𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘0)‘(0 / 𝑁)))
23 fvoveq1 6865 . . . . . . . . . 10 (𝑦 = 0 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(0 / 𝑁)))
2423sneqd 4346 . . . . . . . . 9 (𝑦 = 0 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(0 / 𝑁))})
2524imaeq2d 5648 . . . . . . . 8 (𝑦 = 0 → (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (𝐹 “ {(𝐺‘(0 / 𝑁))}))
2622, 25eleq12d 2838 . . . . . . 7 (𝑦 = 0 → (((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘0)‘(0 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))})))
2719, 26imbi12d 335 . . . . . 6 (𝑦 = 0 → ((𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))}))))
2827imbi2d 331 . . . . 5 (𝑦 = 0 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))})))))
29 eleq1 2832 . . . . . . 7 (𝑦 = 𝑛 → (𝑦 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
30 fveq2 6375 . . . . . . . . 9 (𝑦 = 𝑛 → (𝑄𝑦) = (𝑄𝑛))
31 oveq1 6849 . . . . . . . . 9 (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
3230, 31fveq12d 6382 . . . . . . . 8 (𝑦 = 𝑛 → ((𝑄𝑦)‘(𝑦 / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
33 fvoveq1 6865 . . . . . . . . . 10 (𝑦 = 𝑛 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
3433sneqd 4346 . . . . . . . . 9 (𝑦 = 𝑛 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
3534imaeq2d 5648 . . . . . . . 8 (𝑦 = 𝑛 → (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
3632, 35eleq12d 2838 . . . . . . 7 (𝑦 = 𝑛 → (((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))
3729, 36imbi12d 335 . . . . . 6 (𝑦 = 𝑛 → ((𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (𝑛 ∈ (0...𝑁) → ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
3837imbi2d 331 . . . . 5 (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))))
39 eleq1 2832 . . . . . . 7 (𝑦 = (𝑛 + 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑛 + 1) ∈ (0...𝑁)))
40 fveq2 6375 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (𝑄𝑦) = (𝑄‘(𝑛 + 1)))
41 oveq1 6849 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
4240, 41fveq12d 6382 . . . . . . . 8 (𝑦 = (𝑛 + 1) → ((𝑄𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))
43 fvoveq1 6865 . . . . . . . . . 10 (𝑦 = (𝑛 + 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
4443sneqd 4346 . . . . . . . . 9 (𝑦 = (𝑛 + 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑛 + 1) / 𝑁))})
4544imaeq2d 5648 . . . . . . . 8 (𝑦 = (𝑛 + 1) → (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
4642, 45eleq12d 2838 . . . . . . 7 (𝑦 = (𝑛 + 1) → (((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
4739, 46imbi12d 335 . . . . . 6 (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))))
4847imbi2d 331 . . . . 5 (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
49 eleq1 2832 . . . . . . 7 (𝑦 = (𝑀 − 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑀 − 1) ∈ (0...𝑁)))
50 fveq2 6375 . . . . . . . . 9 (𝑦 = (𝑀 − 1) → (𝑄𝑦) = (𝑄‘(𝑀 − 1)))
51 oveq1 6849 . . . . . . . . 9 (𝑦 = (𝑀 − 1) → (𝑦 / 𝑁) = ((𝑀 − 1) / 𝑁))
5250, 51fveq12d 6382 . . . . . . . 8 (𝑦 = (𝑀 − 1) → ((𝑄𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)))
53 fvoveq1 6865 . . . . . . . . . 10 (𝑦 = (𝑀 − 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑀 − 1) / 𝑁)))
5453sneqd 4346 . . . . . . . . 9 (𝑦 = (𝑀 − 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑀 − 1) / 𝑁))})
5554imaeq2d 5648 . . . . . . . 8 (𝑦 = (𝑀 − 1) → (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
5652, 55eleq12d 2838 . . . . . . 7 (𝑦 = (𝑀 − 1) → (((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
5749, 56imbi12d 335 . . . . . 6 (𝑦 = (𝑀 − 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
5857imbi2d 331 . . . . 5 (𝑦 = (𝑀 − 1) → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄𝑦)‘(𝑦 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))))
59 cvmliftlem.1 . . . . . . . . . . 11 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
60 cvmliftlem.b . . . . . . . . . . 11 𝐵 = 𝐶
61 cvmliftlem.x . . . . . . . . . . 11 𝑋 = 𝐽
62 cvmliftlem.f . . . . . . . . . . 11 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
63 cvmliftlem.g . . . . . . . . . . 11 (𝜑𝐺 ∈ (II Cn 𝐽))
64 cvmliftlem.p . . . . . . . . . . 11 (𝜑𝑃𝐵)
65 cvmliftlem.e . . . . . . . . . . 11 (𝜑 → (𝐹𝑃) = (𝐺‘0))
66 cvmliftlem.t . . . . . . . . . . 11 (𝜑𝑇:(1...𝑁)⟶ 𝑗𝐽 ({𝑗} × (𝑆𝑗)))
67 cvmliftlem.a . . . . . . . . . . 11 (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇𝑘)))
68 cvmliftlem.l . . . . . . . . . . 11 𝐿 = (topGen‘ran (,))
69 cvmliftlem.q . . . . . . . . . . 11 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
7059, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69cvmliftlem4 31718 . . . . . . . . . 10 (𝑄‘0) = {⟨0, 𝑃⟩}
7170a1i 11 . . . . . . . . 9 (𝜑 → (𝑄‘0) = {⟨0, 𝑃⟩})
722nnne0d 11322 . . . . . . . . . 10 (𝜑𝑁 ≠ 0)
733, 72div0d 11054 . . . . . . . . 9 (𝜑 → (0 / 𝑁) = 0)
7471, 73fveq12d 6382 . . . . . . . 8 (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = ({⟨0, 𝑃⟩}‘0))
75 0nn0 11555 . . . . . . . . 9 0 ∈ ℕ0
76 fvsng 6640 . . . . . . . . 9 ((0 ∈ ℕ0𝑃𝐵) → ({⟨0, 𝑃⟩}‘0) = 𝑃)
7775, 64, 76sylancr 581 . . . . . . . 8 (𝜑 → ({⟨0, 𝑃⟩}‘0) = 𝑃)
7874, 77eqtrd 2799 . . . . . . 7 (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = 𝑃)
7973fveq2d 6379 . . . . . . . . 9 (𝜑 → (𝐺‘(0 / 𝑁)) = (𝐺‘0))
8065, 79eqtr4d 2802 . . . . . . . 8 (𝜑 → (𝐹𝑃) = (𝐺‘(0 / 𝑁)))
81 cvmcn 31692 . . . . . . . . . . 11 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
8262, 81syl 17 . . . . . . . . . 10 (𝜑𝐹 ∈ (𝐶 Cn 𝐽))
8360, 61cnf 21330 . . . . . . . . . 10 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵𝑋)
84 ffn 6223 . . . . . . . . . 10 (𝐹:𝐵𝑋𝐹 Fn 𝐵)
8582, 83, 843syl 18 . . . . . . . . 9 (𝜑𝐹 Fn 𝐵)
86 fniniseg 6528 . . . . . . . . 9 (𝐹 Fn 𝐵 → (𝑃 ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃𝐵 ∧ (𝐹𝑃) = (𝐺‘(0 / 𝑁)))))
8785, 86syl 17 . . . . . . . 8 (𝜑 → (𝑃 ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃𝐵 ∧ (𝐹𝑃) = (𝐺‘(0 / 𝑁)))))
8864, 80, 87mpbir2and 704 . . . . . . 7 (𝜑𝑃 ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))}))
8978, 88eqeltrd 2844 . . . . . 6 (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))}))
9089a1d 25 . . . . 5 (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(0 / 𝑁))})))
91 id 22 . . . . . . . . . 10 (𝑛 ∈ ℕ0𝑛 ∈ ℕ0)
92 nn0uz 11922 . . . . . . . . . 10 0 = (ℤ‘0)
9391, 92syl6eleq 2854 . . . . . . . . 9 (𝑛 ∈ ℕ0𝑛 ∈ (ℤ‘0))
9493adantl 473 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ (ℤ‘0))
95 peano2fzr 12561 . . . . . . . . 9 ((𝑛 ∈ (ℤ‘0) ∧ (𝑛 + 1) ∈ (0...𝑁)) → 𝑛 ∈ (0...𝑁))
9695ex 401 . . . . . . . 8 (𝑛 ∈ (ℤ‘0) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
9794, 96syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
9897imim1d 82 . . . . . 6 ((𝜑𝑛 ∈ ℕ0) → ((𝑛 ∈ (0...𝑁) → ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
99 eqid 2765 . . . . . . . . . . 11 ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
100 simprlr 798 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (0...𝑁))
101 elfzle2 12552 . . . . . . . . . . . . 13 ((𝑛 + 1) ∈ (0...𝑁) → (𝑛 + 1) ≤ 𝑁)
102100, 101syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ≤ 𝑁)
103 simprll 797 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℕ0)
104 nn0p1nn 11579 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
105103, 104syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℕ)
106 nnuz 11923 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
107105, 106syl6eleq 2854 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (ℤ‘1))
10812adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℤ)
109 elfz5 12541 . . . . . . . . . . . . 13 (((𝑛 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
110107, 108, 109syl2anc 579 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
111102, 110mpbird 248 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (1...𝑁))
112 simprr 789 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
113103nn0cnd 11600 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℂ)
114 pncan 10541 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
115113, 5, 114sylancl 580 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) − 1) = 𝑛)
116115fveq2d 6379 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄𝑛))
117115oveq1d 6857 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
118116, 117fveq12d 6382 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄𝑛)‘(𝑛 / 𝑁)))
119117fveq2d 6379 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺‘(((𝑛 + 1) − 1) / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
120119sneqd 4346 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
121120imaeq2d 5648 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}) = (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
122112, 118, 1213eltr4d 2859 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}))
12359, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69, 99, 111, 122cvmliftlem6 31720 . . . . . . . . . 10 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
124123simpld 488 . . . . . . . . 9 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
125103nn0red 11599 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℝ)
1262adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℕ)
127125, 126nndivred 11326 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ)
128127rexrd 10343 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ*)
129 peano2re 10463 . . . . . . . . . . . . . 14 (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
130125, 129syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℝ)
131130, 126nndivred 11326 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
132131rexrd 10343 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ*)
133125ltp1d 11208 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 < (𝑛 + 1))
134126nnred 11291 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℝ)
135126nngt0d 11321 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 0 < 𝑁)
136 ltdiv1 11141 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
137125, 130, 134, 135, 136syl112anc 1493 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
138133, 137mpbid 223 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
139127, 131, 138ltled 10439 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
140 ubicc2 12493 . . . . . . . . . . 11 (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
141128, 132, 139, 140syl3anc 1490 . . . . . . . . . 10 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
142117oveq1d 6857 . . . . . . . . . 10 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
143141, 142eleqtrrd 2847 . . . . . . . . 9 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))
144124, 143ffvelrnd 6550 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵)
145123simprd 489 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
146142reseq2d 5565 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
147145, 146eqtrd 2799 . . . . . . . . . 10 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
148147fveq1d 6377 . . . . . . . . 9 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)))
149142feq2d 6209 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
150124, 149mpbid 223 . . . . . . . . . 10 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
151 fvco3 6464 . . . . . . . . . 10 (((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
152150, 141, 151syl2anc 579 . . . . . . . . 9 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
153 fvres 6394 . . . . . . . . . 10 (((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
154141, 153syl 17 . . . . . . . . 9 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
155148, 152, 1543eqtr3d 2807 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))
15685adantr 472 . . . . . . . . 9 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝐹 Fn 𝐵)
157 fniniseg 6528 . . . . . . . . 9 (𝐹 Fn 𝐵 → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))))
158156, 157syl 17 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))))
159144, 155, 158mpbir2and 704 . . . . . . 7 ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
160159expr 448 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁))) → (((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
16198, 160animpimp2impd 872 . . . . 5 (𝑛 ∈ ℕ0 → ((𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄𝑛)‘(𝑛 / 𝑁)) ∈ (𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
16228, 38, 48, 58, 90, 161nn0ind 11719 . . . 4 ((𝑀 − 1) ∈ ℕ0 → (𝜑 → ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
163162impd 398 . . 3 ((𝑀 − 1) ∈ ℕ0 → ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
16418, 163mpcom 38 . 2 ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
16516, 164syldan 585 1 ((𝜑𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315  {csn 4334  cop 4340   cuni 4594   ciun 4676   class class class wbr 4809  cmpt 4888   I cid 5184   × cxp 5275  ccnv 5276  ran crn 5278  cres 5279  cima 5280  ccom 5281   Fn wfn 6063  wf 6064  cfv 6068  crio 6802  (class class class)co 6842  cmpt2 6844  1st c1st 7364  2nd c2nd 7365  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192  *cxr 10327   < clt 10328  cle 10329  cmin 10520   / cdiv 10938  cn 11274  0cn0 11538  cz 11624  cuz 11886  (,)cioo 12377  [,]cicc 12380  ...cfz 12533  seqcseq 13008  t crest 16347  topGenctg 16364   Cn ccn 21308  Homeochmeo 21836  IIcii 22957   CovMap ccvm 31685
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 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
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 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-oadd 7768  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-icc 12384  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-rest 16349  df-topgen 16370  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-top 20978  df-topon 20995  df-bases 21030  df-cn 21311  df-hmeo 21838  df-ii 22959  df-cvm 31686
This theorem is referenced by:  cvmliftlem8  31722  cvmliftlem9  31723  cvmliftlem10  31724  cvmliftlem13  31726
  Copyright terms: Public domain W3C validator