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 35526

Description: Lemma for cvmlift 35534. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 35525 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 13519	. . . 4 ⊢ (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
2		cvmliftlem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	nncnd 12188	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
4	3	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
5		ax-1cn 11094	. . . . . 6 ⊢ 1 ∈ ℂ
6		npcan 11400	. . . . . 6 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
7	4, 5, 6	sylancl 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑁 − 1) + 1) = 𝑁)
8	7	oveq2d 7379	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9	1, 8	sseqtrid 3964	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
10		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
11		elfzelz 13476	. . . . 5 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℤ)
12	2	nnzd 12548	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13		elfzm1b 13554	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
14	11, 12, 13	syl2anr 603	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
15	10, 14	mpbid 233	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
16	9, 15	sseldd 3923	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...𝑁))
17		elfznn0 13572	. . . 4 ⊢ ((𝑀 − 1) ∈ (0...𝑁) → (𝑀 − 1) ∈ ℕ₀)
18	17	adantl 482	. . 3 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → (𝑀 − 1) ∈ ℕ₀)
19		eleq1 2828	. . . . . . 7 ⊢ (𝑦 = 0 → (𝑦 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
20		fveq2 6834	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑄‘𝑦) = (𝑄‘0))
21		oveq1 7370	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑦 / 𝑁) = (0 / 𝑁))
22	20, 21	fveq12d 6841	. . . . . . . 8 ⊢ (𝑦 = 0 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘0)‘(0 / 𝑁)))
23		fvoveq1 7386	. . . . . . . . . 10 ⊢ (𝑦 = 0 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(0 / 𝑁)))
24	23	sneqd 4574	. . . . . . . . 9 ⊢ (𝑦 = 0 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(0 / 𝑁))})
25	24	imaeq2d 6019	. . . . . . . 8 ⊢ (𝑦 = 0 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
26	22, 25	eleq12d 2834	. . . . . . 7 ⊢ (𝑦 = 0 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
27	19, 26	imbi12d 345	. . . . . 6 ⊢ (𝑦 = 0 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))))
28	27	imbi2d 341	. . . . 5 ⊢ (𝑦 = 0 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))))
29		eleq1 2828	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
30		fveq2 6834	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑄‘𝑦) = (𝑄‘𝑛))
31		oveq1 7370	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	30, 31	fveq12d 6841	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
33		fvoveq1 7386	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
34	33	sneqd 4574	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
35	34	imaeq2d 6019	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
36	32, 35	eleq12d 2834	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))
37	29, 36	imbi12d 345	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
38	37	imbi2d 341	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))))
39		eleq1 2828	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑛 + 1) ∈ (0...𝑁)))
40		fveq2 6834	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑄‘𝑦) = (𝑄‘(𝑛 + 1)))
41		oveq1 7370	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
42	40, 41	fveq12d 6841	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))
43		fvoveq1 7386	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
44	43	sneqd 4574	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑛 + 1) / 𝑁))})
45	44	imaeq2d 6019	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
46	42, 45	eleq12d 2834	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
47	39, 46	imbi12d 345	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))))
48	47	imbi2d 341	. . . . 5 ⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
49		eleq1 2828	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑀 − 1) ∈ (0...𝑁)))
50		fveq2 6834	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑄‘𝑦) = (𝑄‘(𝑀 − 1)))
51		oveq1 7370	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 / 𝑁) = ((𝑀 − 1) / 𝑁))
52	50, 51	fveq12d 6841	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)))
53		fvoveq1 7386	. . . . . . . . . 10 ⊢ (𝑦 = (𝑀 − 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑀 − 1) / 𝑁)))
54	53	sneqd 4574	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑀 − 1) / 𝑁))})
55	54	imaeq2d 6019	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
56	52, 55	eleq12d 2834	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
57	49, 56	imbi12d 345	. . . . . 6 ⊢ (𝑦 = (𝑀 − 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
58	57	imbi2d 341	. . . . 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 35523	. . . . . . . . . 10 ⊢ (𝑄‘0) = {⟨0, 𝑃⟩}
71	70	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) = {⟨0, 𝑃⟩})
72	2	nnne0d 12225	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ≠ 0)
73	3, 72	div0d 11928	. . . . . . . . 9 ⊢ (𝜑 → (0 / 𝑁) = 0)
74	71, 73	fveq12d 6841	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = ({⟨0, 𝑃⟩}‘0))
75		0nn0 12450	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
76		fvsng 7131	. . . . . . . . 9 ⊢ ((0 ∈ ℕ₀ ∧ 𝑃 ∈ 𝐵) → ({⟨0, 𝑃⟩}‘0) = 𝑃)
77	75, 64, 76	sylancr 593	. . . . . . . 8 ⊢ (𝜑 → ({⟨0, 𝑃⟩}‘0) = 𝑃)
78	74, 77	eqtrd 2775	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = 𝑃)
79	73	fveq2d 6838	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(0 / 𝑁)) = (𝐺‘0))
80	65, 79	eqtr4d 2778	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))
81		cvmcn 35497	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
82	62, 81	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
83	60, 61	cnf 23236	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋)
84		ffn 6662	. . . . . . . . . 10 ⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵)
85	82, 83, 84	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐵)
86		fniniseg 7008	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐵 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
87	85, 86	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
88	64, 80, 87	mpbir2and 719	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
89	78, 88	eqeltrd 2840	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
90	89	a1d 25	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
91		id 22	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℕ₀)
92		nn0uz 12824	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
93	91, 92	eleqtrdi 2850	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ (ℤ_≥‘0))
94	93	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ (ℤ_≥‘0))
95		peano2fzr 13489	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ℤ_≥‘0) ∧ (𝑛 + 1) ∈ (0...𝑁)) → 𝑛 ∈ (0...𝑁))
96	95	ex 413	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘0) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
97	94, 96	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁)))
98	97	imim1d 82	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
99		eqid 2740	. . . . . . . . . . 11 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
100		simprlr 785	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (0...𝑁))
101		elfzle2 13480	. . . . . . . . . . . . 13 ⊢ ((𝑛 + 1) ∈ (0...𝑁) → (𝑛 + 1) ≤ 𝑁)
102	100, 101	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ≤ 𝑁)
103		simprll 784	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℕ₀)
104		nn0p1nn 12474	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
105	103, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℕ)
106		nnuz 12825	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
107	105, 106	eleqtrdi 2850	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (ℤ_≥‘1))
108	12	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℤ)
109		elfz5 13468	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
110	107, 108, 109	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
111	102, 110	mpbird 258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (1...𝑁))
112		simprr 778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
113	103	nn0cnd 12498	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℂ)
114		pncan 11397	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
115	113, 5, 114	sylancl 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) − 1) = 𝑛)
116	115	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
117	115	oveq1d 7378	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
118	116, 117	fveq12d 6841	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
119	117	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺‘(((𝑛 + 1) − 1) / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
120	119	sneqd 4574	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
121	120	imaeq2d 6019	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
122	112, 118, 121	3eltr4d 2855	. . . . . . . . . . 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 35525	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
124	123	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
125	103	nn0red 12497	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℝ)
126	2	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℕ)
127	125, 126	nndivred 12229	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ)
128	127	rexrd 11193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ^*)
129		peano2re 11317	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
130	125, 129	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℝ)
131	130, 126	nndivred 12229	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
132	131	rexrd 11193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
133	125	ltp1d 12084	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 < (𝑛 + 1))
134	126	nnred 12187	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℝ)
135	126	nngt0d 12224	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 0 < 𝑁)
136		ltdiv1 12018	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
137	125, 130, 134, 135, 136	syl112anc 1382	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
138	133, 137	mpbid 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
139	127, 131, 138	ltled 11292	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
140		ubicc2 13416	. . . . . . . . . . 11 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
141	128, 132, 139, 140	syl3anc 1379	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
142	117	oveq1d 7378	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
143	141, 142	eleqtrrd 2843	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))
144	124, 143	ffvelcdmd 7033	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵)
145	123	simprd 496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
146	142	reseq2d 5938	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
147	145, 146	eqtrd 2775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
148	147	fveq1d 6836	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)))
149	142	feq2d 6646	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
150	124, 149	mpbid 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
151		fvco3 6934	. . . . . . . . . 10 ⊢ (((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
152	150, 141, 151	syl2anc 590	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
153		fvres 6853	. . . . . . . . . 10 ⊢ (((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
154	141, 153	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
155	148, 152, 154	3eqtr3d 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))
156	85	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝐹 Fn 𝐵)
157		fniniseg 7008	. . . . . . . . 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 719	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
160	159	expr 457	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁))) → (((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
161	98, 160	animpimp2impd 852	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
162	28, 38, 48, 58, 90, 161	nn0ind 12622	. . . 4 ⊢ ((𝑀 − 1) ∈ ℕ₀ → (𝜑 → ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))
163	162	impd 411	. . 3 ⊢ ((𝑀 − 1) ∈ ℕ₀ → ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))
164	18, 163	mpcom 38	. 2 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
165	16, 164	syldan 597	1 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ∀wral 3054 {crab 3392 Vcvv 3432 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4268 𝒫 cpw 4536 {csn 4562 ⟨cop 4568 ∪ cuni 4845 ∪ ciun 4928 class class class wbr 5079 ↦ cmpt 5160 I cid 5519 × cxp 5623 ^◡ccnv 5624 ran crn 5626 ↾ cres 5627 “ cima 5628 ∘ ccom 5629 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 ℩crio 7319 (class class class)co 7363 ∈ cmpo 7365 1^st c1st 7936 2^nd c2nd 7937 ℂcc 11034 ℝcr 11035 0cc0 11036 1c1 11037 + caddc 11039 ℝ^*cxr 11176 < clt 11177 ≤ cle 11178 − cmin 11375 / cdiv 11805 ℕcn 12172 ℕ₀cn0 12435 ℤcz 12522 ℤ_≥cuz 12786 (,)cioo 13296 [,]cicc 13299 ...cfz 13459 seqcseq 13961 ↾_t crest 17381 topGenctg 17398 Cn ccn 23214 Homeochmeo 23743 IIcii 24867 CovMap ccvm 35490

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-om 7814 df-1st 7938 df-2nd 7939 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-er 8640 df-map 8772 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fi 9321 df-sup 9352 df-inf 9353 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-n0 12436 df-z 12523 df-uz 12787 df-q 12897 df-rp 12941 df-xneg 13061 df-xadd 13062 df-xmul 13063 df-icc 13303 df-fz 13460 df-seq 13962 df-exp 14022 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-rest 17383 df-topgen 17404 df-psmet 21346 df-xmet 21347 df-met 21348 df-bl 21349 df-mopn 21350 df-top 22884 df-topon 22901 df-bases 22936 df-cn 23217 df-hmeo 23745 df-ii 24869 df-cvm 35491

This theorem is referenced by: cvmliftlem8 35527 cvmliftlem9 35528 cvmliftlem10 35529 cvmliftlem13 35531

W3C validator