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 35278

Description: Lemma for cvmlift 35286. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 35277 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 13528	. . . 4 ⊢ (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
2		cvmliftlem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	nncnd 12202	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
4	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
5		ax-1cn 11126	. . . . . 6 ⊢ 1 ∈ ℂ
6		npcan 11430	. . . . . 6 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
7	4, 5, 6	sylancl 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑁 − 1) + 1) = 𝑁)
8	7	oveq2d 7403	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9	1, 8	sseqtrid 3989	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
10		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
11		elfzelz 13485	. . . . 5 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℤ)
12	2	nnzd 12556	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13		elfzm1b 13563	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
14	11, 12, 13	syl2anr 597	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
15	10, 14	mpbid 232	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
16	9, 15	sseldd 3947	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...𝑁))
17		elfznn0 13581	. . . 4 ⊢ ((𝑀 − 1) ∈ (0...𝑁) → (𝑀 − 1) ∈ ℕ₀)
18	17	adantl 481	. . 3 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → (𝑀 − 1) ∈ ℕ₀)
19		eleq1 2816	. . . . . . 7 ⊢ (𝑦 = 0 → (𝑦 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
20		fveq2 6858	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑄‘𝑦) = (𝑄‘0))
21		oveq1 7394	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑦 / 𝑁) = (0 / 𝑁))
22	20, 21	fveq12d 6865	. . . . . . . 8 ⊢ (𝑦 = 0 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘0)‘(0 / 𝑁)))
23		fvoveq1 7410	. . . . . . . . . 10 ⊢ (𝑦 = 0 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(0 / 𝑁)))
24	23	sneqd 4601	. . . . . . . . 9 ⊢ (𝑦 = 0 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(0 / 𝑁))})
25	24	imaeq2d 6031	. . . . . . . 8 ⊢ (𝑦 = 0 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
26	22, 25	eleq12d 2822	. . . . . . 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 2816	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
30		fveq2 6858	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑄‘𝑦) = (𝑄‘𝑛))
31		oveq1 7394	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	30, 31	fveq12d 6865	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
33		fvoveq1 7410	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
34	33	sneqd 4601	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
35	34	imaeq2d 6031	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
36	32, 35	eleq12d 2822	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))
37	29, 36	imbi12d 344	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
38	37	imbi2d 340	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))))
39		eleq1 2816	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑛 + 1) ∈ (0...𝑁)))
40		fveq2 6858	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑄‘𝑦) = (𝑄‘(𝑛 + 1)))
41		oveq1 7394	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
42	40, 41	fveq12d 6865	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))
43		fvoveq1 7410	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
44	43	sneqd 4601	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑛 + 1) / 𝑁))})
45	44	imaeq2d 6031	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
46	42, 45	eleq12d 2822	. . . . . . 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 2816	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑀 − 1) ∈ (0...𝑁)))
50		fveq2 6858	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑄‘𝑦) = (𝑄‘(𝑀 − 1)))
51		oveq1 7394	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 / 𝑁) = ((𝑀 − 1) / 𝑁))
52	50, 51	fveq12d 6865	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)))
53		fvoveq1 7410	. . . . . . . . . 10 ⊢ (𝑦 = (𝑀 − 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑀 − 1) / 𝑁)))
54	53	sneqd 4601	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑀 − 1) / 𝑁))})
55	54	imaeq2d 6031	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
56	52, 55	eleq12d 2822	. . . . . . 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 35275	. . . . . . . . . 10 ⊢ (𝑄‘0) = {⟨0, 𝑃⟩}
71	70	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) = {⟨0, 𝑃⟩})
72	2	nnne0d 12236	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ≠ 0)
73	3, 72	div0d 11957	. . . . . . . . 9 ⊢ (𝜑 → (0 / 𝑁) = 0)
74	71, 73	fveq12d 6865	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = ({⟨0, 𝑃⟩}‘0))
75		0nn0 12457	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
76		fvsng 7154	. . . . . . . . 9 ⊢ ((0 ∈ ℕ₀ ∧ 𝑃 ∈ 𝐵) → ({⟨0, 𝑃⟩}‘0) = 𝑃)
77	75, 64, 76	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → ({⟨0, 𝑃⟩}‘0) = 𝑃)
78	74, 77	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = 𝑃)
79	73	fveq2d 6862	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(0 / 𝑁)) = (𝐺‘0))
80	65, 79	eqtr4d 2767	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))
81		cvmcn 35249	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
82	62, 81	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
83	60, 61	cnf 23133	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋)
84		ffn 6688	. . . . . . . . . 10 ⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵)
85	82, 83, 84	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐵)
86		fniniseg 7032	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐵 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
87	85, 86	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
88	64, 80, 87	mpbir2and 713	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
89	78, 88	eqeltrd 2828	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
90	89	a1d 25	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
91		id 22	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℕ₀)
92		nn0uz 12835	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
93	91, 92	eleqtrdi 2838	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ (ℤ_≥‘0))
94	93	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ (ℤ_≥‘0))
95		peano2fzr 13498	. . . . . . . . 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 2729	. . . . . . . . . . 11 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
100		simprlr 779	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (0...𝑁))
101		elfzle2 13489	. . . . . . . . . . . . 13 ⊢ ((𝑛 + 1) ∈ (0...𝑁) → (𝑛 + 1) ≤ 𝑁)
102	100, 101	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ≤ 𝑁)
103		simprll 778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℕ₀)
104		nn0p1nn 12481	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
105	103, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℕ)
106		nnuz 12836	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
107	105, 106	eleqtrdi 2838	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (ℤ_≥‘1))
108	12	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℤ)
109		elfz5 13477	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
110	107, 108, 109	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
111	102, 110	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (1...𝑁))
112		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
113	103	nn0cnd 12505	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℂ)
114		pncan 11427	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
115	113, 5, 114	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) − 1) = 𝑛)
116	115	fveq2d 6862	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
117	115	oveq1d 7402	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
118	116, 117	fveq12d 6865	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
119	117	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺‘(((𝑛 + 1) − 1) / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
120	119	sneqd 4601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
121	120	imaeq2d 6031	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
122	112, 118, 121	3eltr4d 2843	. . . . . . . . . . 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 35277	. . . . . . . . . 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 12504	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℝ)
126	2	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℕ)
127	125, 126	nndivred 12240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ)
128	127	rexrd 11224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ^*)
129		peano2re 11347	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
130	125, 129	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℝ)
131	130, 126	nndivred 12240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
132	131	rexrd 11224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
133	125	ltp1d 12113	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 < (𝑛 + 1))
134	126	nnred 12201	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℝ)
135	126	nngt0d 12235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 0 < 𝑁)
136		ltdiv1 12047	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
137	125, 130, 134, 135, 136	syl112anc 1376	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
138	133, 137	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
139	127, 131, 138	ltled 11322	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
140		ubicc2 13426	. . . . . . . . . . 11 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
141	128, 132, 139, 140	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
142	117	oveq1d 7402	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
143	141, 142	eleqtrrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))
144	124, 143	ffvelcdmd 7057	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵)
145	123	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
146	142	reseq2d 5950	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
147	145, 146	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
148	147	fveq1d 6860	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)))
149	142	feq2d 6672	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
150	124, 149	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
151		fvco3 6960	. . . . . . . . . 10 ⊢ (((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
152	150, 141, 151	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
153		fvres 6877	. . . . . . . . . 10 ⊢ (((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
154	141, 153	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
155	148, 152, 154	3eqtr3d 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))
156	85	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝐹 Fn 𝐵)
157		fniniseg 7032	. . . . . . . . 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 713	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
160	159	expr 456	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁))) → (((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
161	98, 160	animpimp2impd 846	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
162	28, 38, 48, 58, 90, 161	nn0ind 12629	. . . 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 591	1 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3044 {crab 3405 Vcvv 3447 ∖ cdif 3911 ∪ cun 3912 ∩ cin 3913 ⊆ wss 3914 ∅c0 4296 𝒫 cpw 4563 {csn 4589 ⟨cop 4595 ∪ cuni 4871 ∪ ciun 4955 class class class wbr 5107 ↦ cmpt 5188 I cid 5532 × cxp 5636 ^◡ccnv 5637 ran crn 5639 ↾ cres 5640 “ cima 5641 ∘ ccom 5642 Fn wfn 6506 ⟶wf 6507 ‘cfv 6511 ℩crio 7343 (class class class)co 7387 ∈ cmpo 7389 1^st c1st 7966 2^nd c2nd 7967 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 ℝ^*cxr 11207 < clt 11208 ≤ cle 11209 − cmin 11405 / cdiv 11835 ℕcn 12186 ℕ₀cn0 12442 ℤcz 12529 ℤ_≥cuz 12793 (,)cioo 13306 [,]cicc 13309 ...cfz 13468 seqcseq 13966 ↾_t crest 17383 topGenctg 17400 Cn ccn 23111 Homeochmeo 23640 IIcii 24768 CovMap ccvm 35242

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-er 8671 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fi 9362 df-sup 9393 df-inf 9394 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-z 12530 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-icc 13313 df-fz 13469 df-seq 13967 df-exp 14027 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-rest 17385 df-topgen 17406 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-top 22781 df-topon 22798 df-bases 22833 df-cn 23114 df-hmeo 23642 df-ii 24770 df-cvm 35243

This theorem is referenced by: cvmliftlem8 35279 cvmliftlem9 35280 cvmliftlem10 35281 cvmliftlem13 35283

W3C validator