cvmliftlem7 - Mathbox for Mario Carneiro

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

Theorem cvmliftlem7 33153

Description: Lemma for cvmlift 33161. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 33152 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) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1^st ‘(𝑇‘𝑘)))
cvmliftlem.l	⊢ 𝐿 = (topGen‘ran (,))
cvmliftlem.q	⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 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.

Step	Hyp	Ref	Expression
1		fzssp1 13228	. . . 4 ⊢ (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
2		cvmliftlem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	nncnd 11919	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
4	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
5		ax-1cn 10860	. . . . . 6 ⊢ 1 ∈ ℂ
6		npcan 11160	. . . . . 6 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
7	4, 5, 6	sylancl 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑁 − 1) + 1) = 𝑁)
8	7	oveq2d 7271	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9	1, 8	sseqtrid 3969	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
10		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
11		elfzelz 13185	. . . . 5 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℤ)
12	2	nnzd 12354	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13		elfzm1b 13263	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
14	11, 12, 13	syl2anr 596	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
15	10, 14	mpbid 231	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
16	9, 15	sseldd 3918	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...𝑁))
17		elfznn0 13278	. . . 4 ⊢ ((𝑀 − 1) ∈ (0...𝑁) → (𝑀 − 1) ∈ ℕ₀)
18	17	adantl 481	. . 3 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → (𝑀 − 1) ∈ ℕ₀)
19		eleq1 2826	. . . . . . 7 ⊢ (𝑦 = 0 → (𝑦 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
20		fveq2 6756	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑄‘𝑦) = (𝑄‘0))
21		oveq1 7262	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑦 / 𝑁) = (0 / 𝑁))
22	20, 21	fveq12d 6763	. . . . . . . 8 ⊢ (𝑦 = 0 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘0)‘(0 / 𝑁)))
23		fvoveq1 7278	. . . . . . . . . 10 ⊢ (𝑦 = 0 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(0 / 𝑁)))
24	23	sneqd 4570	. . . . . . . . 9 ⊢ (𝑦 = 0 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(0 / 𝑁))})
25	24	imaeq2d 5958	. . . . . . . 8 ⊢ (𝑦 = 0 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
26	22, 25	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = 0 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
27	19, 26	imbi12d 344	. . . . . 6 ⊢ (𝑦 = 0 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))))
28	27	imbi2d 340	. . . . 5 ⊢ (𝑦 = 0 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))))
29		eleq1 2826	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
30		fveq2 6756	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑄‘𝑦) = (𝑄‘𝑛))
31		oveq1 7262	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	30, 31	fveq12d 6763	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
33		fvoveq1 7278	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
34	33	sneqd 4570	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
35	34	imaeq2d 5958	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
36	32, 35	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))
37	29, 36	imbi12d 344	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
38	37	imbi2d 340	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))))
39		eleq1 2826	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑛 + 1) ∈ (0...𝑁)))
40		fveq2 6756	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑄‘𝑦) = (𝑄‘(𝑛 + 1)))
41		oveq1 7262	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
42	40, 41	fveq12d 6763	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))
43		fvoveq1 7278	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
44	43	sneqd 4570	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑛 + 1) / 𝑁))})
45	44	imaeq2d 5958	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
46	42, 45	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
47	39, 46	imbi12d 344	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))))
48	47	imbi2d 340	. . . . 5 ⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
49		eleq1 2826	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑀 − 1) ∈ (0...𝑁)))
50		fveq2 6756	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑄‘𝑦) = (𝑄‘(𝑀 − 1)))
51		oveq1 7262	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 / 𝑁) = ((𝑀 − 1) / 𝑁))
52	50, 51	fveq12d 6763	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)))
53		fvoveq1 7278	. . . . . . . . . 10 ⊢ (𝑦 = (𝑀 − 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑀 − 1) / 𝑁)))
54	53	sneqd 4570	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑀 − 1) / 𝑁))})
55	54	imaeq2d 5958	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
56	52, 55	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
57	49, 56	imbi12d 344	. . . . . 6 ⊢ (𝑦 = (𝑀 − 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
58	57	imbi2d 340	. . . . 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) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1^st ‘(𝑇‘𝑘)))
68		cvmliftlem.l	. . . . . . . . . . 11 ⊢ 𝐿 = (topGen‘ran (,))
69		cvmliftlem.q	. . . . . . . . . . 11 ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
70	59, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69	cvmliftlem4 33150	. . . . . . . . . 10 ⊢ (𝑄‘0) = {⟨0, 𝑃⟩}
71	70	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) = {⟨0, 𝑃⟩})
72	2	nnne0d 11953	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ≠ 0)
73	3, 72	div0d 11680	. . . . . . . . 9 ⊢ (𝜑 → (0 / 𝑁) = 0)
74	71, 73	fveq12d 6763	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = ({⟨0, 𝑃⟩}‘0))
75		0nn0 12178	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
76		fvsng 7034	. . . . . . . . 9 ⊢ ((0 ∈ ℕ₀ ∧ 𝑃 ∈ 𝐵) → ({⟨0, 𝑃⟩}‘0) = 𝑃)
77	75, 64, 76	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → ({⟨0, 𝑃⟩}‘0) = 𝑃)
78	74, 77	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = 𝑃)
79	73	fveq2d 6760	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(0 / 𝑁)) = (𝐺‘0))
80	65, 79	eqtr4d 2781	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))
81		cvmcn 33124	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
82	62, 81	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
83	60, 61	cnf 22305	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋)
84		ffn 6584	. . . . . . . . . 10 ⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵)
85	82, 83, 84	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐵)
86		fniniseg 6919	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐵 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
87	85, 86	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
88	64, 80, 87	mpbir2and 709	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
89	78, 88	eqeltrd 2839	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
90	89	a1d 25	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
91		id 22	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℕ₀)
92		nn0uz 12549	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
93	91, 92	eleqtrdi 2849	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ (ℤ_≥‘0))
94	93	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ (ℤ_≥‘0))
95		peano2fzr 13198	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ℤ_≥‘0) ∧ (𝑛 + 1) ∈ (0...𝑁)) → 𝑛 ∈ (0...𝑁))
96	95	ex 412	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘0) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
97	94, 96	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
98	97	imim1d 82	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
99		eqid 2738	. . . . . . . . . . 11 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
100		simprlr 776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (0...𝑁))
101		elfzle2 13189	. . . . . . . . . . . . 13 ⊢ ((𝑛 + 1) ∈ (0...𝑁) → (𝑛 + 1) ≤ 𝑁)
102	100, 101	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ≤ 𝑁)
103		simprll 775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℕ₀)
104		nn0p1nn 12202	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
105	103, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℕ)
106		nnuz 12550	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
107	105, 106	eleqtrdi 2849	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (ℤ_≥‘1))
108	12	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℤ)
109		elfz5 13177	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
110	107, 108, 109	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
111	102, 110	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (1...𝑁))
112		simprr 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
113	103	nn0cnd 12225	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℂ)
114		pncan 11157	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
115	113, 5, 114	sylancl 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) − 1) = 𝑛)
116	115	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
117	115	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
118	116, 117	fveq12d 6763	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
119	117	fveq2d 6760	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺‘(((𝑛 + 1) − 1) / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
120	119	sneqd 4570	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
121	120	imaeq2d 5958	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
122	112, 118, 121	3eltr4d 2854	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}))
123	59, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69, 99, 111, 122	cvmliftlem6 33152	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
124	123	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
125	103	nn0red 12224	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℝ)
126	2	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℕ)
127	125, 126	nndivred 11957	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ)
128	127	rexrd 10956	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ^*)
129		peano2re 11078	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
130	125, 129	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℝ)
131	130, 126	nndivred 11957	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
132	131	rexrd 10956	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
133	125	ltp1d 11835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 < (𝑛 + 1))
134	126	nnred 11918	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℝ)
135	126	nngt0d 11952	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 0 < 𝑁)
136		ltdiv1 11769	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
137	125, 130, 134, 135, 136	syl112anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
138	133, 137	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
139	127, 131, 138	ltled 11053	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
140		ubicc2 13126	. . . . . . . . . . 11 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
141	128, 132, 139, 140	syl3anc 1369	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
142	117	oveq1d 7270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
143	141, 142	eleqtrrd 2842	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))
144	124, 143	ffvelrnd 6944	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵)
145	123	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
146	142	reseq2d 5880	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
147	145, 146	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
148	147	fveq1d 6758	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)))
149	142	feq2d 6570	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
150	124, 149	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
151		fvco3 6849	. . . . . . . . . 10 ⊢ (((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
152	150, 141, 151	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
153		fvres 6775	. . . . . . . . . 10 ⊢ (((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
154	141, 153	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
155	148, 152, 154	3eqtr3d 2786	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))
156	85	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝐹 Fn 𝐵)
157		fniniseg 6919	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐵 → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))))
158	156, 157	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))))
159	144, 155, 158	mpbir2and 709	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
160	159	expr 456	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁))) → (((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
161	98, 160	animpimp2impd 842	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
162	28, 38, 48, 58, 90, 161	nn0ind 12345	. . . 4 ⊢ ((𝑀 − 1) ∈ ℕ₀ → (𝜑 → ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
163	162	impd 410	. . 3 ⊢ ((𝑀 − 1) ∈ ℕ₀ → ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
164	18, 163	mpcom 38	. 2 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
165	16, 164	syldan 590	1 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∀wral 3063 {crab 3067 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 𝒫 cpw 4530 {csn 4558 ⟨cop 4564 ∪ cuni 4836 ∪ ciun 4921 class class class wbr 5070 ↦ cmpt 5153 I cid 5479 × cxp 5578 ^◡ccnv 5579 ran crn 5581 ↾ cres 5582 “ cima 5583 ∘ ccom 5584 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 ℩crio 7211 (class class class)co 7255 ∈ cmpo 7257 1^st c1st 7802 2^nd c2nd 7803 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 / cdiv 11562 ℕcn 11903 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 (,)cioo 13008 [,]cicc 13011 ...cfz 13168 seqcseq 13649 ↾_t crest 17048 topGenctg 17065 Cn ccn 22283 Homeochmeo 22812 IIcii 23944 CovMap ccvm 33117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fi 9100 df-sup 9131 df-inf 9132 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-icc 13015 df-fz 13169 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-rest 17050 df-topgen 17071 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-top 21951 df-topon 21968 df-bases 22004 df-cn 22286 df-hmeo 22814 df-ii 23946 df-cvm 33118

This theorem is referenced by: cvmliftlem8 33154 cvmliftlem9 33155 cvmliftlem10 33156 cvmliftlem13 33158

W3C validator