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 34581

Description: Lemma for cvmlift 34589. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 34580 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 13549	. . . 4 ⊢ (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
2		cvmliftlem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	nncnd 12233	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
4	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
5		ax-1cn 11172	. . . . . 6 ⊢ 1 ∈ ℂ
6		npcan 11474	. . . . . 6 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
7	4, 5, 6	sylancl 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑁 − 1) + 1) = 𝑁)
8	7	oveq2d 7428	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9	1, 8	sseqtrid 4034	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
10		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁))
11		elfzelz 13506	. . . . 5 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℤ)
12	2	nnzd 12590	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℤ)
13		elfzm1b 13584	. . . . 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 3983	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...𝑁))
17		elfznn0 13599	. . . 4 ⊢ ((𝑀 − 1) ∈ (0...𝑁) → (𝑀 − 1) ∈ ℕ₀)
18	17	adantl 481	. . 3 ⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → (𝑀 − 1) ∈ ℕ₀)
19		eleq1 2820	. . . . . . 7 ⊢ (𝑦 = 0 → (𝑦 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁)))
20		fveq2 6891	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑄‘𝑦) = (𝑄‘0))
21		oveq1 7419	. . . . . . . . 9 ⊢ (𝑦 = 0 → (𝑦 / 𝑁) = (0 / 𝑁))
22	20, 21	fveq12d 6898	. . . . . . . 8 ⊢ (𝑦 = 0 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘0)‘(0 / 𝑁)))
23		fvoveq1 7435	. . . . . . . . . 10 ⊢ (𝑦 = 0 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(0 / 𝑁)))
24	23	sneqd 4640	. . . . . . . . 9 ⊢ (𝑦 = 0 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(0 / 𝑁))})
25	24	imaeq2d 6059	. . . . . . . 8 ⊢ (𝑦 = 0 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
26	22, 25	eleq12d 2826	. . . . . . 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 2820	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
30		fveq2 6891	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑄‘𝑦) = (𝑄‘𝑛))
31		oveq1 7419	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	30, 31	fveq12d 6898	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
33		fvoveq1 7435	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
34	33	sneqd 4640	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
35	34	imaeq2d 6059	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
36	32, 35	eleq12d 2826	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))
37	29, 36	imbi12d 344	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))
38	37	imbi2d 340	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))))
39		eleq1 2820	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑛 + 1) ∈ (0...𝑁)))
40		fveq2 6891	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑄‘𝑦) = (𝑄‘(𝑛 + 1)))
41		oveq1 7419	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
42	40, 41	fveq12d 6898	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))
43		fvoveq1 7435	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
44	43	sneqd 4640	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑛 + 1) / 𝑁))})
45	44	imaeq2d 6059	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
46	42, 45	eleq12d 2826	. . . . . . 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 2820	. . . . . . 7 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑀 − 1) ∈ (0...𝑁)))
50		fveq2 6891	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑄‘𝑦) = (𝑄‘(𝑀 − 1)))
51		oveq1 7419	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 / 𝑁) = ((𝑀 − 1) / 𝑁))
52	50, 51	fveq12d 6898	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)))
53		fvoveq1 7435	. . . . . . . . . 10 ⊢ (𝑦 = (𝑀 − 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑀 − 1) / 𝑁)))
54	53	sneqd 4640	. . . . . . . . 9 ⊢ (𝑦 = (𝑀 − 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑀 − 1) / 𝑁))})
55	54	imaeq2d 6059	. . . . . . . 8 ⊢ (𝑦 = (𝑀 − 1) → (^◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
56	52, 55	eleq12d 2826	. . . . . . 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 34578	. . . . . . . . . 10 ⊢ (𝑄‘0) = {⟨0, 𝑃⟩}
71	70	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) = {⟨0, 𝑃⟩})
72	2	nnne0d 12267	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ≠ 0)
73	3, 72	div0d 11994	. . . . . . . . 9 ⊢ (𝜑 → (0 / 𝑁) = 0)
74	71, 73	fveq12d 6898	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = ({⟨0, 𝑃⟩}‘0))
75		0nn0 12492	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
76		fvsng 7180	. . . . . . . . 9 ⊢ ((0 ∈ ℕ₀ ∧ 𝑃 ∈ 𝐵) → ({⟨0, 𝑃⟩}‘0) = 𝑃)
77	75, 64, 76	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → ({⟨0, 𝑃⟩}‘0) = 𝑃)
78	74, 77	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = 𝑃)
79	73	fveq2d 6895	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(0 / 𝑁)) = (𝐺‘0))
80	65, 79	eqtr4d 2774	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))
81		cvmcn 34552	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
82	62, 81	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
83	60, 61	cnf 22971	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋)
84		ffn 6717	. . . . . . . . . 10 ⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵)
85	82, 83, 84	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝐵)
86		fniniseg 7061	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐵 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
87	85, 86	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁)))))
88	64, 80, 87	mpbir2and 710	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
89	78, 88	eqeltrd 2832	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))}))
90	89	a1d 25	. . . . 5 ⊢ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(0 / 𝑁))})))
91		id 22	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℕ₀)
92		nn0uz 12869	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
93	91, 92	eleqtrdi 2842	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ (ℤ_≥‘0))
94	93	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ (ℤ_≥‘0))
95		peano2fzr 13519	. . . . . . . . 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 2731	. . . . . . . . . . 11 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
100		simprlr 777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (0...𝑁))
101		elfzle2 13510	. . . . . . . . . . . . 13 ⊢ ((𝑛 + 1) ∈ (0...𝑁) → (𝑛 + 1) ≤ 𝑁)
102	100, 101	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ≤ 𝑁)
103		simprll 776	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℕ₀)
104		nn0p1nn 12516	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ)
105	103, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℕ)
106		nnuz 12870	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
107	105, 106	eleqtrdi 2842	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (ℤ_≥‘1))
108	12	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℤ)
109		elfz5 13498	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
110	107, 108, 109	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁))
111	102, 110	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (1...𝑁))
112		simprr 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
113	103	nn0cnd 12539	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℂ)
114		pncan 11471	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
115	113, 5, 114	sylancl 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) − 1) = 𝑛)
116	115	fveq2d 6895	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
117	115	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
118	116, 117	fveq12d 6898	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
119	117	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺‘(((𝑛 + 1) − 1) / 𝑁)) = (𝐺‘(𝑛 / 𝑁)))
120	119	sneqd 4640	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))})
121	120	imaeq2d 6059	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}) = (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))
122	112, 118, 121	3eltr4d 2847	. . . . . . . . . . 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 34580	. . . . . . . . . 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 12538	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℝ)
126	2	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℕ)
127	125, 126	nndivred 12271	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ)
128	127	rexrd 11269	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ^*)
129		peano2re 11392	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
130	125, 129	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℝ)
131	130, 126	nndivred 12271	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
132	131	rexrd 11269	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
133	125	ltp1d 12149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 < (𝑛 + 1))
134	126	nnred 12232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℝ)
135	126	nngt0d 12266	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 0 < 𝑁)
136		ltdiv1 12083	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
137	125, 130, 134, 135, 136	syl112anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
138	133, 137	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
139	127, 131, 138	ltled 11367	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
140		ubicc2 13447	. . . . . . . . . . 11 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
141	128, 132, 139, 140	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
142	117	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
143	141, 142	eleqtrrd 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))
144	124, 143	ffvelcdmd 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵)
145	123	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
146	142	reseq2d 5981	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
147	145, 146	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
148	147	fveq1d 6893	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)))
149	142	feq2d 6703	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
150	124, 149	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
151		fvco3 6990	. . . . . . . . . 10 ⊢ (((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
152	150, 141, 151	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))))
153		fvres 6910	. . . . . . . . . 10 ⊢ (((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
154	141, 153	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁)))
155	148, 152, 154	3eqtr3d 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁)))
156	85	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝐹 Fn 𝐵)
157		fniniseg 7061	. . . . . . . . 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 710	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))
160	159	expr 456	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ (0...𝑁))) → (((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))
161	98, 160	animpimp2impd 843	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))))
162	28, 38, 48, 58, 90, 161	nn0ind 12662	. . . 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 1540 ∈ wcel 2105 ∀wral 3060 {crab 3431 Vcvv 3473 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 𝒫 cpw 4602 {csn 4628 ⟨cop 4634 ∪ cuni 4908 ∪ ciun 4997 class class class wbr 5148 ↦ cmpt 5231 I cid 5573 × cxp 5674 ^◡ccnv 5675 ran crn 5677 ↾ cres 5678 “ cima 5679 ∘ ccom 5680 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 ℩crio 7367 (class class class)co 7412 ∈ cmpo 7414 1^st c1st 7977 2^nd c2nd 7978 ℂcc 11112 ℝcr 11113 0cc0 11114 1c1 11115 + caddc 11117 ℝ^*cxr 11252 < clt 11253 ≤ cle 11254 − cmin 11449 / cdiv 11876 ℕcn 12217 ℕ₀cn0 12477 ℤcz 12563 ℤ_≥cuz 12827 (,)cioo 13329 [,]cicc 13332 ...cfz 13489 seqcseq 13971 ↾_t crest 17371 topGenctg 17388 Cn ccn 22949 Homeochmeo 23478 IIcii 24616 CovMap ccvm 34545

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-cnex 11170 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191 ax-pre-sup 11192

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-1st 7979 df-2nd 7980 df-frecs 8270 df-wrecs 8301 df-recs 8375 df-rdg 8414 df-er 8707 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fi 9410 df-sup 9441 df-inf 9442 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-div 11877 df-nn 12218 df-2 12280 df-3 12281 df-n0 12478 df-z 12564 df-uz 12828 df-q 12938 df-rp 12980 df-xneg 13097 df-xadd 13098 df-xmul 13099 df-icc 13336 df-fz 13490 df-seq 13972 df-exp 14033 df-cj 15051 df-re 15052 df-im 15053 df-sqrt 15187 df-abs 15188 df-rest 17373 df-topgen 17394 df-psmet 21137 df-xmet 21138 df-met 21139 df-bl 21140 df-mopn 21141 df-top 22617 df-topon 22634 df-bases 22670 df-cn 22952 df-hmeo 23480 df-ii 24618 df-cvm 34546

This theorem is referenced by: cvmliftlem8 34582 cvmliftlem9 34583 cvmliftlem10 34584 cvmliftlem13 34586

W3C validator