cvmliftlem7

Description: Lemma for cvmlift . Prove by induction that every Q function is well-defined (we can immediately follow this theorem with cvmliftlem6 to show functionality and lifting of Q ). (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmliftlem.b	$⊢ B = ⋃ C$
	cvmliftlem.x	$⊢ X = ⋃ J$
	cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
	cvmliftlem.p	$⊢ φ \to P \in B$
	cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
	cvmliftlem.n	$⊢ φ \to N \in ℕ$
	cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
	cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
	cvmliftlem.l	$⊢ L = topGen (ran (.))$
	cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
	cvmliftlem5.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
Assertion	cvmliftlem7	$⊢ (φ \land M \in (1 \dots N)) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}]$

Proof

Step	Hyp	Ref	Expression
1		cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmliftlem.b	$⊢ B = ⋃ C$
3		cvmliftlem.x	$⊢ X = ⋃ J$
4		cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
6		cvmliftlem.p	$⊢ φ \to P \in B$
7		cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
8		cvmliftlem.n	$⊢ φ \to N \in ℕ$
9		cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
10		cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
11		cvmliftlem.l	$⊢ L = topGen (ran (.))$
12		cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
13		cvmliftlem5.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
14		fzssp1	$⊢ (0 \dots N - 1) \subseteq (0 \dots N - 1 + 1)$
15	8	nncnd	$⊢ φ \to N \in ℂ$
16	15	adantr	$⊢ (φ \land M \in (1 \dots N)) \to N \in ℂ$
17		ax-1cn	$⊢ 1 \in ℂ$
18		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
19	16 17 18	sylancl	$⊢ (φ \land M \in (1 \dots N)) \to N - 1 + 1 = N$
20	19	oveq2d	$⊢ (φ \land M \in (1 \dots N)) \to (0 \dots N - 1 + 1) = (0 \dots N)$
21	14 20	sseqtrid	$⊢ (φ \land M \in (1 \dots N)) \to (0 \dots N - 1) \subseteq (0 \dots N)$
22		simpr	$⊢ (φ \land M \in (1 \dots N)) \to M \in (1 \dots N)$
23		elfzelz	$⊢ M \in (1 \dots N) \to M \in ℤ$
24	8	nnzd	$⊢ φ \to N \in ℤ$
25		elfzm1b	$⊢ (M \in ℤ \land N \in ℤ) \to (M \in (1 \dots N) \leftrightarrow M - 1 \in (0 \dots N - 1))$
26	23 24 25	syl2anr	$⊢ (φ \land M \in (1 \dots N)) \to (M \in (1 \dots N) \leftrightarrow M - 1 \in (0 \dots N - 1))$
27	22 26	mpbid	$⊢ (φ \land M \in (1 \dots N)) \to M - 1 \in (0 \dots N - 1)$
28	21 27	sseldd	$⊢ (φ \land M \in (1 \dots N)) \to M - 1 \in (0 \dots N)$
29		elfznn0	$⊢ M - 1 \in (0 \dots N) \to M - 1 \in ℕ_{0}$
30	29	adantl	$⊢ (φ \land M - 1 \in (0 \dots N)) \to M - 1 \in ℕ_{0}$
31		eleq1	$⊢ y = 0 \to (y \in (0 \dots N) \leftrightarrow 0 \in (0 \dots N))$
32		fveq2	$⊢ y = 0 \to Q (y) = Q (0)$
33		oveq1	$⊢ y = 0 \to \frac{y}{N} = \frac{0}{N}$
34	32 33	fveq12d	$⊢ y = 0 \to Q (y) (\frac{y}{N}) = Q (0) (\frac{0}{N})$
35		fvoveq1	$⊢ y = 0 \to G (\frac{y}{N}) = G (\frac{0}{N})$
36	35	sneqd	$⊢ y = 0 \to \{G (\frac{y}{N})\} = \{G (\frac{0}{N})\}$
37	36	imaeq2d	$⊢ y = 0 \to F^{-1} [\{G (\frac{y}{N})\}] = F^{-1} [\{G (\frac{0}{N})\}]$
38	34 37	eleq12d	$⊢ y = 0 \to (Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}] \leftrightarrow Q (0) (\frac{0}{N}) \in F^{-1} [\{G (\frac{0}{N})\}])$
39	31 38	imbi12d	$⊢ y = 0 \to ((y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}]) \leftrightarrow (0 \in (0 \dots N) \to Q (0) (\frac{0}{N}) \in F^{-1} [\{G (\frac{0}{N})\}]))$
40	39	imbi2d	$⊢ y = 0 \to ((φ \to (y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}])) \leftrightarrow (φ \to (0 \in (0 \dots N) \to Q (0) (\frac{0}{N}) \in F^{-1} [\{G (\frac{0}{N})\}])))$
41		eleq1	$⊢ y = n \to (y \in (0 \dots N) \leftrightarrow n \in (0 \dots N))$
42		fveq2	$⊢ y = n \to Q (y) = Q (n)$
43		oveq1	$⊢ y = n \to \frac{y}{N} = \frac{n}{N}$
44	42 43	fveq12d	$⊢ y = n \to Q (y) (\frac{y}{N}) = Q (n) (\frac{n}{N})$
45		fvoveq1	$⊢ y = n \to G (\frac{y}{N}) = G (\frac{n}{N})$
46	45	sneqd	$⊢ y = n \to \{G (\frac{y}{N})\} = \{G (\frac{n}{N})\}$
47	46	imaeq2d	$⊢ y = n \to F^{-1} [\{G (\frac{y}{N})\}] = F^{-1} [\{G (\frac{n}{N})\}]$
48	44 47	eleq12d	$⊢ y = n \to (Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}] \leftrightarrow Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])$
49	41 48	imbi12d	$⊢ y = n \to ((y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}]) \leftrightarrow (n \in (0 \dots N) \to Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}]))$
50	49	imbi2d	$⊢ y = n \to ((φ \to (y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}])) \leftrightarrow (φ \to (n \in (0 \dots N) \to Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])))$
51		eleq1	$⊢ y = n + 1 \to (y \in (0 \dots N) \leftrightarrow n + 1 \in (0 \dots N))$
52		fveq2	$⊢ y = n + 1 \to Q (y) = Q (n + 1)$
53		oveq1	$⊢ y = n + 1 \to \frac{y}{N} = \frac{n + 1}{N}$
54	52 53	fveq12d	$⊢ y = n + 1 \to Q (y) (\frac{y}{N}) = Q (n + 1) (\frac{n + 1}{N})$
55		fvoveq1	$⊢ y = n + 1 \to G (\frac{y}{N}) = G (\frac{n + 1}{N})$
56	55	sneqd	$⊢ y = n + 1 \to \{G (\frac{y}{N})\} = \{G (\frac{n + 1}{N})\}$
57	56	imaeq2d	$⊢ y = n + 1 \to F^{-1} [\{G (\frac{y}{N})\}] = F^{-1} [\{G (\frac{n + 1}{N})\}]$
58	54 57	eleq12d	$⊢ y = n + 1 \to (Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}] \leftrightarrow Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}])$
59	51 58	imbi12d	$⊢ y = n + 1 \to ((y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}]) \leftrightarrow (n + 1 \in (0 \dots N) \to Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}]))$
60	59	imbi2d	$⊢ y = n + 1 \to ((φ \to (y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}])) \leftrightarrow (φ \to (n + 1 \in (0 \dots N) \to Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}])))$
61		eleq1	$⊢ y = M - 1 \to (y \in (0 \dots N) \leftrightarrow M - 1 \in (0 \dots N))$
62		fveq2	$⊢ y = M - 1 \to Q (y) = Q (M - 1)$
63		oveq1	$⊢ y = M - 1 \to \frac{y}{N} = \frac{M - 1}{N}$
64	62 63	fveq12d	$⊢ y = M - 1 \to Q (y) (\frac{y}{N}) = Q (M - 1) (\frac{M - 1}{N})$
65		fvoveq1	$⊢ y = M - 1 \to G (\frac{y}{N}) = G (\frac{M - 1}{N})$
66	65	sneqd	$⊢ y = M - 1 \to \{G (\frac{y}{N})\} = \{G (\frac{M - 1}{N})\}$
67	66	imaeq2d	$⊢ y = M - 1 \to F^{-1} [\{G (\frac{y}{N})\}] = F^{-1} [\{G (\frac{M - 1}{N})\}]$
68	64 67	eleq12d	$⊢ y = M - 1 \to (Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}] \leftrightarrow Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}])$
69	61 68	imbi12d	$⊢ y = M - 1 \to ((y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}]) \leftrightarrow (M - 1 \in (0 \dots N) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}]))$
70	69	imbi2d	$⊢ y = M - 1 \to ((φ \to (y \in (0 \dots N) \to Q (y) (\frac{y}{N}) \in F^{-1} [\{G (\frac{y}{N})\}])) \leftrightarrow (φ \to (M - 1 \in (0 \dots N) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}])))$
71	1 2 3 4 5 6 7 8 9 10 11 12	cvmliftlem4	$⊢ Q (0) = \{⟨0, P⟩\}$
72	71	a1i	$⊢ φ \to Q (0) = \{⟨0, P⟩\}$
73	8	nnne0d	$⊢ φ \to N \neq 0$
74	15 73	div0d	$⊢ φ \to \frac{0}{N} = 0$
75	72 74	fveq12d	$⊢ φ \to Q (0) (\frac{0}{N}) = \{⟨0, P⟩\} (0)$
76		0nn0	$⊢ 0 \in ℕ_{0}$
77		fvsng	$⊢ (0 \in ℕ_{0} \land P \in B) \to \{⟨0, P⟩\} (0) = P$
78	76 6 77	sylancr	$⊢ φ \to \{⟨0, P⟩\} (0) = P$
79	75 78	eqtrd	$⊢ φ \to Q (0) (\frac{0}{N}) = P$
80	74	fveq2d	$⊢ φ \to G (\frac{0}{N}) = G (0)$
81	7 80	eqtr4d	$⊢ φ \to F (P) = G (\frac{0}{N})$
82		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
83	4 82	syl	$⊢ φ \to F \in (C Cn J)$
84	2 3	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ X$
85		ffn	$⊢ F : B ⟶ X \to F Fn B$
86	83 84 85	3syl	$⊢ φ \to F Fn B$
87		fniniseg	$⊢ F Fn B \to (P \in F^{-1} [\{G (\frac{0}{N})\}] \leftrightarrow (P \in B \land F (P) = G (\frac{0}{N})))$
88	86 87	syl	$⊢ φ \to (P \in F^{-1} [\{G (\frac{0}{N})\}] \leftrightarrow (P \in B \land F (P) = G (\frac{0}{N})))$
89	6 81 88	mpbir2and	$⊢ φ \to P \in F^{-1} [\{G (\frac{0}{N})\}]$
90	79 89	eqeltrd	$⊢ φ \to Q (0) (\frac{0}{N}) \in F^{-1} [\{G (\frac{0}{N})\}]$
91	90	a1d	$⊢ φ \to (0 \in (0 \dots N) \to Q (0) (\frac{0}{N}) \in F^{-1} [\{G (\frac{0}{N})\}])$
92		id	$⊢ n \in ℕ_{0} \to n \in ℕ_{0}$
93		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
94	92 93	eleqtrdi	$⊢ n \in ℕ_{0} \to n \in ℤ_{\geq 0}$
95	94	adantl	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℤ_{\geq 0}$
96		peano2fzr	$⊢ (n \in ℤ_{\geq 0} \land n + 1 \in (0 \dots N)) \to n \in (0 \dots N)$
97	96	ex	$⊢ n \in ℤ_{\geq 0} \to (n + 1 \in (0 \dots N) \to n \in (0 \dots N))$
98	95 97	syl	$⊢ (φ \land n \in ℕ_{0}) \to (n + 1 \in (0 \dots N) \to n \in (0 \dots N))$
99	98	imim1d	$⊢ (φ \land n \in ℕ_{0}) \to ((n \in (0 \dots N) \to Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}]) \to (n + 1 \in (0 \dots N) \to Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}]))$
100		eqid	$⊢ [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] = [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]$
101		simprlr	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n + 1 \in (0 \dots N)$
102		elfzle2	$⊢ n + 1 \in (0 \dots N) \to n + 1 \leq N$
103	101 102	syl	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n + 1 \leq N$
104		simprll	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n \in ℕ_{0}$
105		nn0p1nn	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ$
106	104 105	syl	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n + 1 \in ℕ$
107		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
108	106 107	eleqtrdi	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n + 1 \in ℤ_{\geq 1}$
109	24	adantr	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to N \in ℤ$
110		elfz5	$⊢ (n + 1 \in ℤ_{\geq 1} \land N \in ℤ) \to (n + 1 \in (1 \dots N) \leftrightarrow n + 1 \leq N)$
111	108 109 110	syl2anc	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (n + 1 \in (1 \dots N) \leftrightarrow n + 1 \leq N)$
112	103 111	mpbird	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n + 1 \in (1 \dots N)$
113		simprr	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}]$
114	104	nn0cnd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n \in ℂ$
115		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
116	114 17 115	sylancl	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n + 1 - 1 = n$
117	116	fveq2d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n + 1 - 1) = Q (n)$
118	116	oveq1d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n + 1 - 1}{N} = \frac{n}{N}$
119	117 118	fveq12d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n + 1 - 1) (\frac{n + 1 - 1}{N}) = Q (n) (\frac{n}{N})$
120	118	fveq2d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to G (\frac{n + 1 - 1}{N}) = G (\frac{n}{N})$
121	120	sneqd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \{G (\frac{n + 1 - 1}{N})\} = \{G (\frac{n}{N})\}$
122	121	imaeq2d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to F^{-1} [\{G (\frac{n + 1 - 1}{N})\}] = F^{-1} [\{G (\frac{n}{N})\}]$
123	113 119 122	3eltr4d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n + 1 - 1) (\frac{n + 1 - 1}{N}) \in F^{-1} [\{G (\frac{n + 1 - 1}{N})\}]$
124	1 2 3 4 5 6 7 8 9 10 11 12 100 112 123	cvmliftlem6	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (Q (n + 1) : [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] ⟶ B \land F \circ Q (n + 1) = {G ↾}_{[\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]})$
125	124	simpld	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n + 1) : [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] ⟶ B$
126	104	nn0red	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n \in ℝ$
127	8	adantr	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to N \in ℕ$
128	126 127	nndivred	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n}{N} \in ℝ$
129	128	rexrd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n}{N} \in ℝ^{*}$
130		peano2re	$⊢ n \in ℝ \to n + 1 \in ℝ$
131	126 130	syl	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n + 1 \in ℝ$
132	131 127	nndivred	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n + 1}{N} \in ℝ$
133	132	rexrd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n + 1}{N} \in ℝ^{*}$
134	126	ltp1d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to n < n + 1$
135	127	nnred	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to N \in ℝ$
136	127	nngt0d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to 0 < N$
137		ltdiv1	$⊢ (n \in ℝ \land n + 1 \in ℝ \land (N \in ℝ \land 0 < N)) \to (n < n + 1 \leftrightarrow \frac{n}{N} < \frac{n + 1}{N})$
138	126 131 135 136 137	syl112anc	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (n < n + 1 \leftrightarrow \frac{n}{N} < \frac{n + 1}{N})$
139	134 138	mpbid	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n}{N} < \frac{n + 1}{N}$
140	128 132 139	ltled	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n}{N} \leq \frac{n + 1}{N}$
141		ubicc2	$⊢ (\frac{n}{N} \in ℝ^{} \land \frac{n + 1}{N} \in ℝ^{} \land \frac{n}{N} \leq \frac{n + 1}{N}) \to \frac{n + 1}{N} \in [\frac{n}{N}, \frac{n + 1}{N}]$
142	129 133 140 141	syl3anc	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n + 1}{N} \in [\frac{n}{N}, \frac{n + 1}{N}]$
143	118	oveq1d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] = [\frac{n}{N}, \frac{n + 1}{N}]$
144	142 143	eleqtrrd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to \frac{n + 1}{N} \in [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]$
145	125 144	ffvelcdmd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n + 1) (\frac{n + 1}{N}) \in B$
146	124	simprd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to F \circ Q (n + 1) = {G ↾}_{[\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]}$
147	143	reseq2d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to {G ↾}_{[\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]} = {G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}$
148	146 147	eqtrd	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to F \circ Q (n + 1) = {G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}$
149	148	fveq1d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (F \circ Q (n + 1)) (\frac{n + 1}{N}) = ({G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}) (\frac{n + 1}{N})$
150	143	feq2d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (Q (n + 1) : [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] ⟶ B \leftrightarrow Q (n + 1) : [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B)$
151	125 150	mpbid	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n + 1) : [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B$
152		fvco3	$⊢ (Q (n + 1) : [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B \land \frac{n + 1}{N} \in [\frac{n}{N}, \frac{n + 1}{N}]) \to (F \circ Q (n + 1)) (\frac{n + 1}{N}) = F (Q (n + 1) (\frac{n + 1}{N}))$
153	151 142 152	syl2anc	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (F \circ Q (n + 1)) (\frac{n + 1}{N}) = F (Q (n + 1) (\frac{n + 1}{N}))$
154		fvres	$⊢ \frac{n + 1}{N} \in [\frac{n}{N}, \frac{n + 1}{N}] \to ({G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}) (\frac{n + 1}{N}) = G (\frac{n + 1}{N})$
155	142 154	syl	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to ({G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}) (\frac{n + 1}{N}) = G (\frac{n + 1}{N})$
156	149 153 155	3eqtr3d	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to F (Q (n + 1) (\frac{n + 1}{N})) = G (\frac{n + 1}{N})$
157	86	adantr	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to F Fn B$
158		fniniseg	$⊢ F Fn B \to (Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}] \leftrightarrow (Q (n + 1) (\frac{n + 1}{N}) \in B \land F (Q (n + 1) (\frac{n + 1}{N})) = G (\frac{n + 1}{N})))$
159	157 158	syl	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}] \leftrightarrow (Q (n + 1) (\frac{n + 1}{N}) \in B \land F (Q (n + 1) (\frac{n + 1}{N})) = G (\frac{n + 1}{N})))$
160	145 156 159	mpbir2and	$⊢ (φ \land ((n \in ℕ_{0} \land n + 1 \in (0 \dots N)) \land Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}]$
161	160	expr	$⊢ (φ \land (n \in ℕ_{0} \land n + 1 \in (0 \dots N))) \to (Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}] \to Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}])$
162	99 161	animpimp2impd	$⊢ n \in ℕ_{0} \to ((φ \to (n \in (0 \dots N) \to Q (n) (\frac{n}{N}) \in F^{-1} [\{G (\frac{n}{N})\}])) \to (φ \to (n + 1 \in (0 \dots N) \to Q (n + 1) (\frac{n + 1}{N}) \in F^{-1} [\{G (\frac{n + 1}{N})\}])))$
163	40 50 60 70 91 162	nn0ind	$⊢ M - 1 \in ℕ_{0} \to (φ \to (M - 1 \in (0 \dots N) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}]))$
164	163	impd	$⊢ M - 1 \in ℕ_{0} \to ((φ \land M - 1 \in (0 \dots N)) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}])$
165	30 164	mpcom	$⊢ (φ \land M - 1 \in (0 \dots N)) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}]$
166	28 165	syldan	$⊢ (φ \land M \in (1 \dots N)) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}]$

Metamath Proof Explorer

Theorem cvmliftlem7

Proof