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 35878

Description: Lemma for cvmlift 35886. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 35877 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 13626	. . . 4 ⊢ (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
2		cvmliftlem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	nncnd 12277	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
4	3	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
5		ax-1cn 11186	. . . . . 6 ⊢ 1 ∈ ℂ
6		npcan 11494	. . . . . 6 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
7	4, 5, 6	sylancl 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑁 − 1) + 1) = 𝑁)
8	7	oveq2d 7433	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9	1, 8	sseqtrid 3976	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
10		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
11		elfzelz 13582	. . . . 5 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℤ)
12	2	nnzd 12645	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13		elfzm1b 13661	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
14	11, 12, 13	syl2anr 609	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
15	10, 14	mpbid 235	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
16	9, 15	sseldd 3935	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...𝑁))
17		elfznn0 13679	. . . 4 ⊢ ((𝑀 − 1) ∈ (0...𝑁) → (𝑀 − 1) ∈ ℕ₀)
18	17	adantl 487	. . 3 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → (𝑀 − 1) ∈ ℕ₀)
19		eleq1 2850	. . . . . . 7 ⊢ (𝑦 = 0 → (𝑦 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
20		fveq2 6882	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑄‘𝑦) = (𝑄‘0))
21		oveq1 7424	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑦 / 𝑁) = (0 / 𝑁))
22	20, 21	fveq12d 6889	. . . . . . . 8 ⊢ (𝑦 = 0 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘0)‘(0 / 𝑁)))
23		fvoveq1 7440	. . . . . . . . . 10 ⊢ (𝑦 = 0 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(0 / 𝑁)))
24	23	sneqd 4599	. . . . . . . . 9 ⊢ (𝑦 = 0 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(0 / 𝑁))})
25	24	imaeq2d 6060	. . . . . . . 8 ⊢ (𝑦 = 0 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
26	22, 25	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = 0 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
27	19, 26	imbi12d 347	. . . . . 6 ⊢ (𝑦 = 0 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))))
28	27	imbi2d 343	. . . . 5 ⊢ (𝑦 = 0 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))))
29		eleq1 2850	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
30		fveq2 6882	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑄‘𝑦) = (𝑄‘𝑛))
31		oveq1 7424	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	30, 31	fveq12d 6889	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
33		fvoveq1 7440	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
34	33	sneqd 4599	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
35	34	imaeq2d 6060	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
36	32, 35	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))
37	29, 36	imbi12d 347	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
38	37	imbi2d 343	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))))
39		eleq1 2850	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑛 + 1) ∈ (0...𝑁)))
40		fveq2 6882	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑄‘𝑦) = (𝑄‘(𝑛 + 1)))
41		oveq1 7424	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
42	40, 41	fveq12d 6889	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))
43		fvoveq1 7440	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
44	43	sneqd 4599	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑛 + 1) / 𝑁))})
45	44	imaeq2d 6060	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
46	42, 45	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
47	39, 46	imbi12d 347	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))))
48	47	imbi2d 343	. . . . 5 ⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
49		eleq1 2850	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑀 − 1) ∈ (0...𝑁)))
50		fveq2 6882	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑄‘𝑦) = (𝑄‘(𝑀 − 1)))
51		oveq1 7424	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 / 𝑁) = ((𝑀 − 1) / 𝑁))
52	50, 51	fveq12d 6889	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)))
53		fvoveq1 7440	. . . . . . . . . 10 ⊢ (𝑦 = (𝑀 − 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑀 − 1) / 𝑁)))
54	53	sneqd 4599	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑀 − 1) / 𝑁))})
55	54	imaeq2d 6060	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
56	52, 55	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
57	49, 56	imbi12d 347	. . . . . 6 ⊢ (𝑦 = (𝑀 − 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
58	57	imbi2d 343	. . . . 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 35875	. . . . . . . . . 10 ⊢ (𝑄‘0) = {⟨0, 𝑃⟩}
71	70	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) = {⟨0, 𝑃⟩})
72	2	nnne0d 12314	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ≠ 0)
73	3, 72	div0d 12018	. . . . . . . . 9 ⊢ (𝜑 → (0 / 𝑁) = 0)
74	71, 73	fveq12d 6889	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = ({⟨0, 𝑃⟩}‘0))
75		0nn0 12547	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
76		fvsng 7182	. . . . . . . . 9 ⊢ ((0 ∈ ℕ₀ ∧ 𝑃 ∈ 𝐵) → ({⟨0, 𝑃⟩}‘0) = 𝑃)
77	75, 64, 76	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → ({⟨0, 𝑃⟩}‘0) = 𝑃)
78	74, 77	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = 𝑃)
79	73	fveq2d 6886	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(0 / 𝑁)) = (𝐺‘0))
80	65, 79	eqtr4d 2800	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))
81		cvmcn 35849	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
82	62, 81	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
83	60, 61	cnf 23477	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋)
84		ffn 6706	. . . . . . . . . 10 ⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵)
85	82, 83, 84	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐵)
86		fniniseg 7056	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐵 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
87	85, 86	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
88	64, 80, 87	mpbir2and 726	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
89	78, 88	eqeltrd 2862	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
90	89	a1d 26	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
91		id 23	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℕ₀)
92		nn0uz 12929	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
93	91, 92	eleqtrdi 2872	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ (ℤ_≥‘0))
94	93	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ (ℤ_≥‘0))
95		peano2fzr 13595	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ℤ_≥‘0) ∧ (𝑛 + 1) ∈ (0...𝑁)) → 𝑛 ∈ (0...𝑁))
96	95	ex 418	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘0) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
97	94, 96	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
98	97	imim1d 83	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
99		eqid 2762	. . . . . . . . . . 11 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
100		simprlr 792	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (0...𝑁))
101		elfzle2 13586	. . . . . . . . . . . . 13 ⊢ ((𝑛 + 1) ∈ (0...𝑁) → (𝑛 + 1) ≤ 𝑁)
102	100, 101	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ≤ 𝑁)
103		simprll 791	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℕ₀)
104		nn0p1nn 12571	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
105	103, 104	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℕ)
106		nnuz 12930	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
107	105, 106	eleqtrdi 2872	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (ℤ_≥‘1))
108	12	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℤ)
109		elfz5 13574	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
110	107, 108, 109	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
111	102, 110	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (1...𝑁))
112		simprr 785	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
113	103	nn0cnd 12595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℂ)
114		pncan 11491	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
115	113, 5, 114	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) − 1) = 𝑛)
116	115	fveq2d 6886	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
117	115	oveq1d 7432	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
118	116, 117	fveq12d 6889	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
119	117	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺‘(((𝑛 + 1) − 1) / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
120	119	sneqd 4599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
121	120	imaeq2d 6060	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
122	112, 118, 121	3eltr4d 2877	. . . . . . . . . . 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 35877	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
124	123	simpld 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
125	103	nn0red 12594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℝ)
126	2	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℕ)
127	125, 126	nndivred 12318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ)
128	127	rexrd 11287	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ^*)
129		peano2re 11411	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
130	125, 129	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℝ)
131	130, 126	nndivred 12318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
132	131	rexrd 11287	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
133	125	ltp1d 12173	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 < (𝑛 + 1))
134	126	nnred 12276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℝ)
135	126	nngt0d 12313	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 0 < 𝑁)
136		ltdiv1 12107	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
137	125, 130, 134, 135, 136	syl112anc 1401	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
138	133, 137	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
139	127, 131, 138	ltled 11386	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
140		ubicc2 13522	. . . . . . . . . . 11 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
141	128, 132, 139, 140	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
142	117	oveq1d 7432	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
143	141, 142	eleqtrrd 2865	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))
144	124, 143	ffvelcdmd 7082	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵)
145	123	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
146	142	reseq2d 5976	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
147	145, 146	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
148	147	fveq1d 6884	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)))
149	142	feq2d 6690	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
150	124, 149	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
151		fvco3 6982	. . . . . . . . . 10 ⊢ (((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
152	150, 141, 151	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
153		fvres 6901	. . . . . . . . . 10 ⊢ (((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
154	141, 153	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
155	148, 152, 154	3eqtr3d 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))
156	85	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝐹 Fn 𝐵)
157		fniniseg 7056	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐵 → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))))
158	156, 157	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))))
159	144, 155, 158	mpbir2and 726	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
160	159	expr 462	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁))) → (((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
161	98, 160	animpimp2impd 860	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
162	28, 38, 48, 58, 90, 161	nn0ind 12720	. . . 4 ⊢ ((𝑀 − 1) ∈ ℕ₀ → (𝜑 → ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
163	162	impd 416	. . 3 ⊢ ((𝑀 − 1) ∈ ℕ₀ → ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
164	18, 163	mpcom 39	. 2 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
165	16, 164	syldan 603	1 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3078 {crab 3414 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 𝒫 cpw 4560 {csn 4587 ⟨cop 4593 ∪ cuni 4870 ∪ ciun 4954 class class class wbr 5107 ↦ cmpt 5190 I cid 5553 × cxp 5657 ^◡ccnv 5658 ran crn 5660 ↾ cres 5661 “ cima 5662 ∘ ccom 5663 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 ℩crio 7373 (class class class)co 7417 ∈ cmpo 7419 1^st c1st 7988 2^nd c2nd 7989 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 ℝ^*cxr 11270 < clt 11271 ≤ cle 11272 − cmin 11469 / cdiv 11899 ℕcn 12261 ℕ₀cn0 12532 ℤcz 12619 ℤ_≥cuz 12891 (,)cioo 13402 [,]cicc 13405 ...cfz 13565 seqcseq 14069 ↾_t crest 17511 topGenctg 17528 Cn ccn 23455 Homeochmeo 23985 IIcii 25109 CovMap ccvm 35842

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-er 8700 df-map 8832 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fi 9385 df-sup 9416 df-inf 9417 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-n0 12533 df-z 12620 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-icc 13409 df-fz 13566 df-seq 14070 df-exp 14130 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-rest 17513 df-topgen 17534 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-top 23125 df-topon 23142 df-bases 23177 df-cn 23458 df-hmeo 23987 df-ii 25111 df-cvm 35843

This theorem is used by: cvmliftlem8 35879 cvmliftlem9 35880 cvmliftlem10 35881 cvmliftlem13 35883

W3C validator