cvmliftlem10

Description: Lemma for cvmlift . The function K is going to be our complete lifted path, formed by unioning together all the Q functions (each of which is defined on one segment [ ( M - 1 ) / N , M / N ] of the interval). Here we prove by induction that K is a continuous function and a lift of G by applying cvmliftlem6 , cvmliftlem7 (to show it is a function and a lift), cvmliftlem8 (to show it is continuous), and cvmliftlem9 (to show that different Q functions agree on the intersection of their domains, so that the pasting lemma paste gives that K is well-defined and continuous). (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⟩\}⟩\}))$
	cvmliftlem.k	$⊢ K = ⋃_{k = 1}^{N} Q (k)$
	cvmliftlem10.1	$⊢ χ \leftrightarrow ((n \in ℕ \land n + 1 \in (1 \dots N)) \land (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}))$
Assertion	cvmliftlem10	$⊢ φ \to (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{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		cvmliftlem.k	$⊢ K = ⋃_{k = 1}^{N} Q (k)$
14		cvmliftlem10.1	$⊢ χ \leftrightarrow ((n \in ℕ \land n + 1 \in (1 \dots N)) \land (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}))$
15		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
16	8 15	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
17		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
18	16 17	syl	$⊢ φ \to N \in (1 \dots N)$
19		eleq1	$⊢ y = 1 \to (y \in (1 \dots N) \leftrightarrow 1 \in (1 \dots N))$
20		oveq2	$⊢ y = 1 \to (1 \dots y) = (1 \dots 1)$
21		1z	$⊢ 1 \in ℤ$
22		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
23	21 22	ax-mp	$⊢ (1 \dots 1) = \{1\}$
24	20 23	eqtrdi	$⊢ y = 1 \to (1 \dots y) = \{1\}$
25	24	iuneq1d	$⊢ y = 1 \to ⋃_{k = 1}^{y} Q (k) = ⋃_{k \in \{1\}} Q (k)$
26		1ex	$⊢ 1 \in V$
27		fveq2	$⊢ k = 1 \to Q (k) = Q (1)$
28	26 27	iunxsn	$⊢ ⋃_{k \in \{1\}} Q (k) = Q (1)$
29	25 28	eqtrdi	$⊢ y = 1 \to ⋃_{k = 1}^{y} Q (k) = Q (1)$
30		oveq1	$⊢ y = 1 \to \frac{y}{N} = \frac{1}{N}$
31	30	oveq2d	$⊢ y = 1 \to [0, \frac{y}{N}] = [0, \frac{1}{N}]$
32	31	oveq2d	$⊢ y = 1 \to L ↾_{𝑡} [0, \frac{y}{N}] = L ↾_{𝑡} [0, \frac{1}{N}]$
33	32	oveq1d	$⊢ y = 1 \to (L ↾_{𝑡} [0, \frac{y}{N}]) Cn C = (L ↾_{𝑡} [0, \frac{1}{N}]) Cn C$
34	29 33	eleq12d	$⊢ y = 1 \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \leftrightarrow Q (1) \in ((L ↾_{𝑡} [0, \frac{1}{N}]) Cn C))$
35	29	coeq2d	$⊢ y = 1 \to F \circ ⋃_{k = 1}^{y} Q (k) = F \circ Q (1)$
36	31	reseq2d	$⊢ y = 1 \to {G ↾}_{[0, \frac{y}{N}]} = {G ↾}_{[0, \frac{1}{N}]}$
37	35 36	eqeq12d	$⊢ y = 1 \to (F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]} \leftrightarrow F \circ Q (1) = {G ↾}_{[0, \frac{1}{N}]})$
38	34 37	anbi12d	$⊢ y = 1 \to ((⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}) \leftrightarrow (Q (1) \in ((L ↾_{𝑡} [0, \frac{1}{N}]) Cn C) \land F \circ Q (1) = {G ↾}_{[0, \frac{1}{N}]}))$
39	19 38	imbi12d	$⊢ y = 1 \to ((y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]})) \leftrightarrow (1 \in (1 \dots N) \to (Q (1) \in ((L ↾_{𝑡} [0, \frac{1}{N}]) Cn C) \land F \circ Q (1) = {G ↾}_{[0, \frac{1}{N}]})))$
40	39	imbi2d	$⊢ y = 1 \to ((φ \to (y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}))) \leftrightarrow (φ \to (1 \in (1 \dots N) \to (Q (1) \in ((L ↾_{𝑡} [0, \frac{1}{N}]) Cn C) \land F \circ Q (1) = {G ↾}_{[0, \frac{1}{N}]}))))$
41		eleq1	$⊢ y = n \to (y \in (1 \dots N) \leftrightarrow n \in (1 \dots N))$
42		oveq2	$⊢ y = n \to (1 \dots y) = (1 \dots n)$
43	42	iuneq1d	$⊢ y = n \to ⋃_{k = 1}^{y} Q (k) = ⋃_{k = 1}^{n} Q (k)$
44		oveq1	$⊢ y = n \to \frac{y}{N} = \frac{n}{N}$
45	44	oveq2d	$⊢ y = n \to [0, \frac{y}{N}] = [0, \frac{n}{N}]$
46	45	oveq2d	$⊢ y = n \to L ↾_{𝑡} [0, \frac{y}{N}] = L ↾_{𝑡} [0, \frac{n}{N}]$
47	46	oveq1d	$⊢ y = n \to (L ↾_{𝑡} [0, \frac{y}{N}]) Cn C = (L ↾_{𝑡} [0, \frac{n}{N}]) Cn C$
48	43 47	eleq12d	$⊢ y = n \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \leftrightarrow ⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C))$
49	43	coeq2d	$⊢ y = n \to F \circ ⋃_{k = 1}^{y} Q (k) = F \circ ⋃_{k = 1}^{n} Q (k)$
50	45	reseq2d	$⊢ y = n \to {G ↾}_{[0, \frac{y}{N}]} = {G ↾}_{[0, \frac{n}{N}]}$
51	49 50	eqeq12d	$⊢ y = n \to (F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]} \leftrightarrow F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]})$
52	48 51	anbi12d	$⊢ y = n \to ((⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}) \leftrightarrow (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}))$
53	41 52	imbi12d	$⊢ y = n \to ((y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]})) \leftrightarrow (n \in (1 \dots N) \to (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]})))$
54	53	imbi2d	$⊢ y = n \to ((φ \to (y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}))) \leftrightarrow (φ \to (n \in (1 \dots N) \to (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}))))$
55		eleq1	$⊢ y = n + 1 \to (y \in (1 \dots N) \leftrightarrow n + 1 \in (1 \dots N))$
56		oveq2	$⊢ y = n + 1 \to (1 \dots y) = (1 \dots n + 1)$
57	56	iuneq1d	$⊢ y = n + 1 \to ⋃_{k = 1}^{y} Q (k) = ⋃_{k = 1}^{n + 1} Q (k)$
58		oveq1	$⊢ y = n + 1 \to \frac{y}{N} = \frac{n + 1}{N}$
59	58	oveq2d	$⊢ y = n + 1 \to [0, \frac{y}{N}] = [0, \frac{n + 1}{N}]$
60	59	oveq2d	$⊢ y = n + 1 \to L ↾_{𝑡} [0, \frac{y}{N}] = L ↾_{𝑡} [0, \frac{n + 1}{N}]$
61	60	oveq1d	$⊢ y = n + 1 \to (L ↾_{𝑡} [0, \frac{y}{N}]) Cn C = (L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C$
62	57 61	eleq12d	$⊢ y = n + 1 \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \leftrightarrow ⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C))$
63	57	coeq2d	$⊢ y = n + 1 \to F \circ ⋃_{k = 1}^{y} Q (k) = F \circ ⋃_{k = 1}^{n + 1} Q (k)$
64	59	reseq2d	$⊢ y = n + 1 \to {G ↾}_{[0, \frac{y}{N}]} = {G ↾}_{[0, \frac{n + 1}{N}]}$
65	63 64	eqeq12d	$⊢ y = n + 1 \to (F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]} \leftrightarrow F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]})$
66	62 65	anbi12d	$⊢ y = n + 1 \to ((⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}) \leftrightarrow (⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]}))$
67	55 66	imbi12d	$⊢ y = n + 1 \to ((y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]})) \leftrightarrow (n + 1 \in (1 \dots N) \to (⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]})))$
68	67	imbi2d	$⊢ y = n + 1 \to ((φ \to (y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}))) \leftrightarrow (φ \to (n + 1 \in (1 \dots N) \to (⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]}))))$
69		eleq1	$⊢ y = N \to (y \in (1 \dots N) \leftrightarrow N \in (1 \dots N))$
70		oveq2	$⊢ y = N \to (1 \dots y) = (1 \dots N)$
71	70	iuneq1d	$⊢ y = N \to ⋃_{k = 1}^{y} Q (k) = ⋃_{k = 1}^{N} Q (k)$
72	71 13	eqtr4di	$⊢ y = N \to ⋃_{k = 1}^{y} Q (k) = K$
73		oveq1	$⊢ y = N \to \frac{y}{N} = \frac{N}{N}$
74	73	oveq2d	$⊢ y = N \to [0, \frac{y}{N}] = [0, \frac{N}{N}]$
75	74	oveq2d	$⊢ y = N \to L ↾_{𝑡} [0, \frac{y}{N}] = L ↾_{𝑡} [0, \frac{N}{N}]$
76	75	oveq1d	$⊢ y = N \to (L ↾_{𝑡} [0, \frac{y}{N}]) Cn C = (L ↾_{𝑡} [0, \frac{N}{N}]) Cn C$
77	72 76	eleq12d	$⊢ y = N \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \leftrightarrow K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C))$
78	72	coeq2d	$⊢ y = N \to F \circ ⋃_{k = 1}^{y} Q (k) = F \circ K$
79	74	reseq2d	$⊢ y = N \to {G ↾}_{[0, \frac{y}{N}]} = {G ↾}_{[0, \frac{N}{N}]}$
80	78 79	eqeq12d	$⊢ y = N \to (F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]} \leftrightarrow F \circ K = {G ↾}_{[0, \frac{N}{N}]})$
81	77 80	anbi12d	$⊢ y = N \to ((⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}) \leftrightarrow (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{N}]}))$
82	69 81	imbi12d	$⊢ y = N \to ((y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]})) \leftrightarrow (N \in (1 \dots N) \to (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{N}]})))$
83	82	imbi2d	$⊢ y = N \to ((φ \to (y \in (1 \dots N) \to (⋃_{k = 1}^{y} Q (k) \in ((L ↾_{𝑡} [0, \frac{y}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{y} Q (k) = {G ↾}_{[0, \frac{y}{N}]}))) \leftrightarrow (φ \to (N \in (1 \dots N) \to (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{N}]}))))$
84		eluzfz1	$⊢ N \in ℤ_{\geq 1} \to 1 \in (1 \dots N)$
85	16 84	syl	$⊢ φ \to 1 \in (1 \dots N)$
86		eqid	$⊢ [\frac{1 - 1}{N}, \frac{1}{N}] = [\frac{1 - 1}{N}, \frac{1}{N}]$
87	1 2 3 4 5 6 7 8 9 10 11 12 86	cvmliftlem8	$⊢ (φ \land 1 \in (1 \dots N)) \to Q (1) \in ((L ↾_{𝑡} [\frac{1 - 1}{N}, \frac{1}{N}]) Cn C)$
88	85 87	mpdan	$⊢ φ \to Q (1) \in ((L ↾_{𝑡} [\frac{1 - 1}{N}, \frac{1}{N}]) Cn C)$
89		1m1e0	$⊢ 1 - 1 = 0$
90	89	oveq1i	$⊢ \frac{1 - 1}{N} = \frac{0}{N}$
91	8	nncnd	$⊢ φ \to N \in ℂ$
92	8	nnne0d	$⊢ φ \to N \neq 0$
93	91 92	div0d	$⊢ φ \to \frac{0}{N} = 0$
94	90 93	syl5eq	$⊢ φ \to \frac{1 - 1}{N} = 0$
95	94	oveq1d	$⊢ φ \to [\frac{1 - 1}{N}, \frac{1}{N}] = [0, \frac{1}{N}]$
96	95	oveq2d	$⊢ φ \to L ↾_{𝑡} [\frac{1 - 1}{N}, \frac{1}{N}] = L ↾_{𝑡} [0, \frac{1}{N}]$
97	96	oveq1d	$⊢ φ \to (L ↾_{𝑡} [\frac{1 - 1}{N}, \frac{1}{N}]) Cn C = (L ↾_{𝑡} [0, \frac{1}{N}]) Cn C$
98	88 97	eleqtrd	$⊢ φ \to Q (1) \in ((L ↾_{𝑡} [0, \frac{1}{N}]) Cn C)$
99		simpr	$⊢ (φ \land 1 \in (1 \dots N)) \to 1 \in (1 \dots N)$
100	1 2 3 4 5 6 7 8 9 10 11 12 86	cvmliftlem7	$⊢ (φ \land 1 \in (1 \dots N)) \to Q (1 - 1) (\frac{1 - 1}{N}) \in F^{-1} [\{G (\frac{1 - 1}{N})\}]$
101	1 2 3 4 5 6 7 8 9 10 11 12 86 99 100	cvmliftlem6	$⊢ (φ \land 1 \in (1 \dots N)) \to (Q (1) : [\frac{1 - 1}{N}, \frac{1}{N}] ⟶ B \land F \circ Q (1) = {G ↾}_{[\frac{1 - 1}{N}, \frac{1}{N}]})$
102	85 101	mpdan	$⊢ φ \to (Q (1) : [\frac{1 - 1}{N}, \frac{1}{N}] ⟶ B \land F \circ Q (1) = {G ↾}_{[\frac{1 - 1}{N}, \frac{1}{N}]})$
103	102	simprd	$⊢ φ \to F \circ Q (1) = {G ↾}_{[\frac{1 - 1}{N}, \frac{1}{N}]}$
104	95	reseq2d	$⊢ φ \to {G ↾}_{[\frac{1 - 1}{N}, \frac{1}{N}]} = {G ↾}_{[0, \frac{1}{N}]}$
105	103 104	eqtrd	$⊢ φ \to F \circ Q (1) = {G ↾}_{[0, \frac{1}{N}]}$
106	98 105	jca	$⊢ φ \to (Q (1) \in ((L ↾_{𝑡} [0, \frac{1}{N}]) Cn C) \land F \circ Q (1) = {G ↾}_{[0, \frac{1}{N}]})$
107	106	a1d	$⊢ φ \to (1 \in (1 \dots N) \to (Q (1) \in ((L ↾_{𝑡} [0, \frac{1}{N}]) Cn C) \land F \circ Q (1) = {G ↾}_{[0, \frac{1}{N}]}))$
108		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
109	108	biimpi	$⊢ n \in ℕ \to n \in ℤ_{\geq 1}$
110	109	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℤ_{\geq 1}$
111		peano2fzr	$⊢ (n \in ℤ_{\geq 1} \land n + 1 \in (1 \dots N)) \to n \in (1 \dots N)$
112	111	ex	$⊢ n \in ℤ_{\geq 1} \to (n + 1 \in (1 \dots N) \to n \in (1 \dots N))$
113	110 112	syl	$⊢ (φ \land n \in ℕ) \to (n + 1 \in (1 \dots N) \to n \in (1 \dots N))$
114	113	imim1d	$⊢ (φ \land n \in ℕ) \to ((n \in (1 \dots N) \to (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]})) \to (n + 1 \in (1 \dots N) \to (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]})))$
115		eqid	$⊢ ⋃ (L ↾_{𝑡} [0, \frac{n + 1}{N}]) = ⋃ (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
116		0re	$⊢ 0 \in ℝ$
117	14	simplbi	$⊢ χ \to (n \in ℕ \land n + 1 \in (1 \dots N))$
118	117	adantl	$⊢ (φ \land χ) \to (n \in ℕ \land n + 1 \in (1 \dots N))$
119	118	simprd	$⊢ (φ \land χ) \to n + 1 \in (1 \dots N)$
120		elfznn	$⊢ n + 1 \in (1 \dots N) \to n + 1 \in ℕ$
121	119 120	syl	$⊢ (φ \land χ) \to n + 1 \in ℕ$
122	121	nnred	$⊢ (φ \land χ) \to n + 1 \in ℝ$
123	8	adantr	$⊢ (φ \land χ) \to N \in ℕ$
124	122 123	nndivred	$⊢ (φ \land χ) \to \frac{n + 1}{N} \in ℝ$
125		iccssre	$⊢ (0 \in ℝ \land \frac{n + 1}{N} \in ℝ) \to [0, \frac{n + 1}{N}] \subseteq ℝ$
126	116 124 125	sylancr	$⊢ (φ \land χ) \to [0, \frac{n + 1}{N}] \subseteq ℝ$
127	117	simpld	$⊢ χ \to n \in ℕ$
128	127	adantl	$⊢ (φ \land χ) \to n \in ℕ$
129	128	nnred	$⊢ (φ \land χ) \to n \in ℝ$
130	129 123	nndivred	$⊢ (φ \land χ) \to \frac{n}{N} \in ℝ$
131		icccld	$⊢ (0 \in ℝ \land \frac{n}{N} \in ℝ) \to [0, \frac{n}{N}] \in Clsd (topGen (ran (.)))$
132	116 130 131	sylancr	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \in Clsd (topGen (ran (.)))$
133	11	fveq2i	$⊢ Clsd (L) = Clsd (topGen (ran (.)))$
134	132 133	eleqtrrdi	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \in Clsd (L)$
135		ssun1	$⊢ [0, \frac{n}{N}] \subseteq [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}]$
136	116	a1i	$⊢ (φ \land χ) \to 0 \in ℝ$
137	128	nnnn0d	$⊢ (φ \land χ) \to n \in ℕ_{0}$
138	137	nn0ge0d	$⊢ (φ \land χ) \to 0 \leq n$
139	123	nnred	$⊢ (φ \land χ) \to N \in ℝ$
140	123	nngt0d	$⊢ (φ \land χ) \to 0 < N$
141		divge0	$⊢ ((n \in ℝ \land 0 \leq n) \land (N \in ℝ \land 0 < N)) \to 0 \leq \frac{n}{N}$
142	129 138 139 140 141	syl22anc	$⊢ (φ \land χ) \to 0 \leq \frac{n}{N}$
143	129	ltp1d	$⊢ (φ \land χ) \to n < n + 1$
144		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})$
145	129 122 139 140 144	syl112anc	$⊢ (φ \land χ) \to (n < n + 1 \leftrightarrow \frac{n}{N} < \frac{n + 1}{N})$
146	143 145	mpbid	$⊢ (φ \land χ) \to \frac{n}{N} < \frac{n + 1}{N}$
147	130 124 146	ltled	$⊢ (φ \land χ) \to \frac{n}{N} \leq \frac{n + 1}{N}$
148		elicc2	$⊢ (0 \in ℝ \land \frac{n + 1}{N} \in ℝ) \to (\frac{n}{N} \in [0, \frac{n + 1}{N}] \leftrightarrow (\frac{n}{N} \in ℝ \land 0 \leq \frac{n}{N} \land \frac{n}{N} \leq \frac{n + 1}{N}))$
149	116 124 148	sylancr	$⊢ (φ \land χ) \to (\frac{n}{N} \in [0, \frac{n + 1}{N}] \leftrightarrow (\frac{n}{N} \in ℝ \land 0 \leq \frac{n}{N} \land \frac{n}{N} \leq \frac{n + 1}{N}))$
150	130 142 147 149	mpbir3and	$⊢ (φ \land χ) \to \frac{n}{N} \in [0, \frac{n + 1}{N}]$
151		iccsplit	$⊢ (0 \in ℝ \land \frac{n + 1}{N} \in ℝ \land \frac{n}{N} \in [0, \frac{n + 1}{N}]) \to [0, \frac{n + 1}{N}] = [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}]$
152	136 124 150 151	syl3anc	$⊢ (φ \land χ) \to [0, \frac{n + 1}{N}] = [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}]$
153	135 152	sseqtrrid	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \subseteq [0, \frac{n + 1}{N}]$
154		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
155	11	unieqi	$⊢ ⋃ L = ⋃ topGen (ran (.))$
156	154 155	eqtr4i	$⊢ ℝ = ⋃ L$
157	156	restcldi	$⊢ ([0, \frac{n + 1}{N}] \subseteq ℝ \land [0, \frac{n}{N}] \in Clsd (L) \land [0, \frac{n}{N}] \subseteq [0, \frac{n + 1}{N}]) \to [0, \frac{n}{N}] \in Clsd (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
158	126 134 153 157	syl3anc	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \in Clsd (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
159		icccld	$⊢ (\frac{n}{N} \in ℝ \land \frac{n + 1}{N} \in ℝ) \to [\frac{n}{N}, \frac{n + 1}{N}] \in Clsd (topGen (ran (.)))$
160	130 124 159	syl2anc	$⊢ (φ \land χ) \to [\frac{n}{N}, \frac{n + 1}{N}] \in Clsd (topGen (ran (.)))$
161	160 133	eleqtrrdi	$⊢ (φ \land χ) \to [\frac{n}{N}, \frac{n + 1}{N}] \in Clsd (L)$
162		ssun2	$⊢ [\frac{n}{N}, \frac{n + 1}{N}] \subseteq [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}]$
163	162 152	sseqtrrid	$⊢ (φ \land χ) \to [\frac{n}{N}, \frac{n + 1}{N}] \subseteq [0, \frac{n + 1}{N}]$
164	156	restcldi	$⊢ ([0, \frac{n + 1}{N}] \subseteq ℝ \land [\frac{n}{N}, \frac{n + 1}{N}] \in Clsd (L) \land [\frac{n}{N}, \frac{n + 1}{N}] \subseteq [0, \frac{n + 1}{N}]) \to [\frac{n}{N}, \frac{n + 1}{N}] \in Clsd (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
165	126 161 163 164	syl3anc	$⊢ (φ \land χ) \to [\frac{n}{N}, \frac{n + 1}{N}] \in Clsd (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
166		retop	$⊢ topGen (ran (.)) \in Top$
167	11 166	eqeltri	$⊢ L \in Top$
168	156	restuni	$⊢ (L \in Top \land [0, \frac{n + 1}{N}] \subseteq ℝ) \to [0, \frac{n + 1}{N}] = ⋃ (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
169	167 126 168	sylancr	$⊢ (φ \land χ) \to [0, \frac{n + 1}{N}] = ⋃ (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
170	152 169	eqtr3d	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}] = ⋃ (L ↾_{𝑡} [0, \frac{n + 1}{N}])$
171	14	simprbi	$⊢ χ \to (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]})$
172	171	adantl	$⊢ (φ \land χ) \to (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]})$
173	172	simpld	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C)$
174		eqid	$⊢ ⋃ (L ↾_{𝑡} [0, \frac{n}{N}]) = ⋃ (L ↾_{𝑡} [0, \frac{n}{N}])$
175	174 2	cnf	$⊢ ⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \to ⋃_{k = 1}^{n} Q (k) : ⋃ (L ↾_{𝑡} [0, \frac{n}{N}]) ⟶ B$
176	173 175	syl	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n} Q (k) : ⋃ (L ↾_{𝑡} [0, \frac{n}{N}]) ⟶ B$
177		iccssre	$⊢ (0 \in ℝ \land \frac{n}{N} \in ℝ) \to [0, \frac{n}{N}] \subseteq ℝ$
178	116 130 177	sylancr	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \subseteq ℝ$
179	156	restuni	$⊢ (L \in Top \land [0, \frac{n}{N}] \subseteq ℝ) \to [0, \frac{n}{N}] = ⋃ (L ↾_{𝑡} [0, \frac{n}{N}])$
180	167 178 179	sylancr	$⊢ (φ \land χ) \to [0, \frac{n}{N}] = ⋃ (L ↾_{𝑡} [0, \frac{n}{N}])$
181	180	feq2d	$⊢ (φ \land χ) \to (⋃_{k = 1}^{n} Q (k) : [0, \frac{n}{N}] ⟶ B \leftrightarrow ⋃_{k = 1}^{n} Q (k) : ⋃ (L ↾_{𝑡} [0, \frac{n}{N}]) ⟶ B)$
182	176 181	mpbird	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n} Q (k) : [0, \frac{n}{N}] ⟶ B$
183		eqid	$⊢ [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] = [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]$
184		simpr	$⊢ (φ \land n + 1 \in (1 \dots N)) \to n + 1 \in (1 \dots N)$
185	1 2 3 4 5 6 7 8 9 10 11 12 183	cvmliftlem7	$⊢ (φ \land n + 1 \in (1 \dots N)) \to Q (n + 1 - 1) (\frac{n + 1 - 1}{N}) \in F^{-1} [\{G (\frac{n + 1 - 1}{N})\}]$
186	1 2 3 4 5 6 7 8 9 10 11 12 183 184 185	cvmliftlem6	$⊢ (φ \land n + 1 \in (1 \dots 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}]})$
187	119 186	syldan	$⊢ (φ \land χ) \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}]})$
188	187	simpld	$⊢ (φ \land χ) \to Q (n + 1) : [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] ⟶ B$
189	128	nncnd	$⊢ (φ \land χ) \to n \in ℂ$
190		ax-1cn	$⊢ 1 \in ℂ$
191		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
192	189 190 191	sylancl	$⊢ (φ \land χ) \to n + 1 - 1 = n$
193	192	oveq1d	$⊢ (φ \land χ) \to \frac{n + 1 - 1}{N} = \frac{n}{N}$
194	193	oveq1d	$⊢ (φ \land χ) \to [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] = [\frac{n}{N}, \frac{n + 1}{N}]$
195	194	feq2d	$⊢ (φ \land χ) \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)$
196	188 195	mpbid	$⊢ (φ \land χ) \to Q (n + 1) : [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B$
197	176	ffund	$⊢ (φ \land χ) \to Fun ⋃_{k = 1}^{n} Q (k)$
198	128 109	syl	$⊢ (φ \land χ) \to n \in ℤ_{\geq 1}$
199		eluzfz2	$⊢ n \in ℤ_{\geq 1} \to n \in (1 \dots n)$
200	198 199	syl	$⊢ (φ \land χ) \to n \in (1 \dots n)$
201		fveq2	$⊢ k = n \to Q (k) = Q (n)$
202	201	ssiun2s	$⊢ n \in (1 \dots n) \to Q (n) \subseteq ⋃_{k = 1}^{n} Q (k)$
203	200 202	syl	$⊢ (φ \land χ) \to Q (n) \subseteq ⋃_{k = 1}^{n} Q (k)$
204		peano2rem	$⊢ n \in ℝ \to n - 1 \in ℝ$
205	129 204	syl	$⊢ (φ \land χ) \to n - 1 \in ℝ$
206	205 123	nndivred	$⊢ (φ \land χ) \to \frac{n - 1}{N} \in ℝ$
207	206	rexrd	$⊢ (φ \land χ) \to \frac{n - 1}{N} \in ℝ^{*}$
208	130	rexrd	$⊢ (φ \land χ) \to \frac{n}{N} \in ℝ^{*}$
209	129	ltm1d	$⊢ (φ \land χ) \to n - 1 < n$
210		ltdiv1	$⊢ (n - 1 \in ℝ \land n \in ℝ \land (N \in ℝ \land 0 < N)) \to (n - 1 < n \leftrightarrow \frac{n - 1}{N} < \frac{n}{N})$
211	205 129 139 140 210	syl112anc	$⊢ (φ \land χ) \to (n - 1 < n \leftrightarrow \frac{n - 1}{N} < \frac{n}{N})$
212	209 211	mpbid	$⊢ (φ \land χ) \to \frac{n - 1}{N} < \frac{n}{N}$
213	206 130 212	ltled	$⊢ (φ \land χ) \to \frac{n - 1}{N} \leq \frac{n}{N}$
214		ubicc2	$⊢ (\frac{n - 1}{N} \in ℝ^{} \land \frac{n}{N} \in ℝ^{} \land \frac{n - 1}{N} \leq \frac{n}{N}) \to \frac{n}{N} \in [\frac{n - 1}{N}, \frac{n}{N}]$
215	207 208 213 214	syl3anc	$⊢ (φ \land χ) \to \frac{n}{N} \in [\frac{n - 1}{N}, \frac{n}{N}]$
216	198 119 111	syl2anc	$⊢ (φ \land χ) \to n \in (1 \dots N)$
217		eqid	$⊢ [\frac{n - 1}{N}, \frac{n}{N}] = [\frac{n - 1}{N}, \frac{n}{N}]$
218		simpr	$⊢ (φ \land n \in (1 \dots N)) \to n \in (1 \dots N)$
219	1 2 3 4 5 6 7 8 9 10 11 12 217	cvmliftlem7	$⊢ (φ \land n \in (1 \dots N)) \to Q (n - 1) (\frac{n - 1}{N}) \in F^{-1} [\{G (\frac{n - 1}{N})\}]$
220	1 2 3 4 5 6 7 8 9 10 11 12 217 218 219	cvmliftlem6	$⊢ (φ \land n \in (1 \dots N)) \to (Q (n) : [\frac{n - 1}{N}, \frac{n}{N}] ⟶ B \land F \circ Q (n) = {G ↾}_{[\frac{n - 1}{N}, \frac{n}{N}]})$
221	216 220	syldan	$⊢ (φ \land χ) \to (Q (n) : [\frac{n - 1}{N}, \frac{n}{N}] ⟶ B \land F \circ Q (n) = {G ↾}_{[\frac{n - 1}{N}, \frac{n}{N}]})$
222	221	simpld	$⊢ (φ \land χ) \to Q (n) : [\frac{n - 1}{N}, \frac{n}{N}] ⟶ B$
223	222	fdmd	$⊢ (φ \land χ) \to dom Q (n) = [\frac{n - 1}{N}, \frac{n}{N}]$
224	215 223	eleqtrrd	$⊢ (φ \land χ) \to \frac{n}{N} \in dom Q (n)$
225		funssfv	$⊢ (Fun ⋃_{k = 1}^{n} Q (k) \land Q (n) \subseteq ⋃_{k = 1}^{n} Q (k) \land \frac{n}{N} \in dom Q (n)) \to ⋃_{k = 1}^{n} Q (k) (\frac{n}{N}) = Q (n) (\frac{n}{N})$
226	197 203 224 225	syl3anc	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n} Q (k) (\frac{n}{N}) = Q (n) (\frac{n}{N})$
227	192	fveq2d	$⊢ (φ \land χ) \to Q (n + 1 - 1) = Q (n)$
228	227 193	fveq12d	$⊢ (φ \land χ) \to Q (n + 1 - 1) (\frac{n + 1 - 1}{N}) = Q (n) (\frac{n}{N})$
229	1 2 3 4 5 6 7 8 9 10 11 12	cvmliftlem9	$⊢ (φ \land n + 1 \in (1 \dots N)) \to Q (n + 1) (\frac{n + 1 - 1}{N}) = Q (n + 1 - 1) (\frac{n + 1 - 1}{N})$
230	119 229	syldan	$⊢ (φ \land χ) \to Q (n + 1) (\frac{n + 1 - 1}{N}) = Q (n + 1 - 1) (\frac{n + 1 - 1}{N})$
231	193	fveq2d	$⊢ (φ \land χ) \to Q (n + 1) (\frac{n + 1 - 1}{N}) = Q (n + 1) (\frac{n}{N})$
232	230 231	eqtr3d	$⊢ (φ \land χ) \to Q (n + 1 - 1) (\frac{n + 1 - 1}{N}) = Q (n + 1) (\frac{n}{N})$
233	226 228 232	3eqtr2d	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n} Q (k) (\frac{n}{N}) = Q (n + 1) (\frac{n}{N})$
234	233	opeq2d	$⊢ (φ \land χ) \to ⟨\frac{n}{N}, ⋃_{k = 1}^{n} Q (k) (\frac{n}{N})⟩ = ⟨\frac{n}{N}, Q (n + 1) (\frac{n}{N})⟩$
235	234	sneqd	$⊢ (φ \land χ) \to \{⟨\frac{n}{N}, ⋃_{k = 1}^{n} Q (k) (\frac{n}{N})⟩\} = \{⟨\frac{n}{N}, Q (n + 1) (\frac{n}{N})⟩\}$
236	182	ffnd	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n} Q (k) Fn [0, \frac{n}{N}]$
237		0xr	$⊢ 0 \in ℝ^{*}$
238	237	a1i	$⊢ (φ \land χ) \to 0 \in ℝ^{*}$
239		ubicc2	$⊢ (0 \in ℝ^{} \land \frac{n}{N} \in ℝ^{} \land 0 \leq \frac{n}{N}) \to \frac{n}{N} \in [0, \frac{n}{N}]$
240	238 208 142 239	syl3anc	$⊢ (φ \land χ) \to \frac{n}{N} \in [0, \frac{n}{N}]$
241		fnressn	$⊢ (⋃_{k = 1}^{n} Q (k) Fn [0, \frac{n}{N}] \land \frac{n}{N} \in [0, \frac{n}{N}]) \to {⋃_{k = 1}^{n} Q (k) ↾}_{\{\frac{n}{N}\}} = \{⟨\frac{n}{N}, ⋃_{k = 1}^{n} Q (k) (\frac{n}{N})⟩\}$
242	236 240 241	syl2anc	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n} Q (k) ↾}_{\{\frac{n}{N}\}} = \{⟨\frac{n}{N}, ⋃_{k = 1}^{n} Q (k) (\frac{n}{N})⟩\}$
243	196	ffnd	$⊢ (φ \land χ) \to Q (n + 1) Fn [\frac{n}{N}, \frac{n + 1}{N}]$
244	124	rexrd	$⊢ (φ \land χ) \to \frac{n + 1}{N} \in ℝ^{*}$
245		lbicc2	$⊢ (\frac{n}{N} \in ℝ^{} \land \frac{n + 1}{N} \in ℝ^{} \land \frac{n}{N} \leq \frac{n + 1}{N}) \to \frac{n}{N} \in [\frac{n}{N}, \frac{n + 1}{N}]$
246	208 244 147 245	syl3anc	$⊢ (φ \land χ) \to \frac{n}{N} \in [\frac{n}{N}, \frac{n + 1}{N}]$
247		fnressn	$⊢ (Q (n + 1) Fn [\frac{n}{N}, \frac{n + 1}{N}] \land \frac{n}{N} \in [\frac{n}{N}, \frac{n + 1}{N}]) \to {Q (n + 1) ↾}_{\{\frac{n}{N}\}} = \{⟨\frac{n}{N}, Q (n + 1) (\frac{n}{N})⟩\}$
248	243 246 247	syl2anc	$⊢ (φ \land χ) \to {Q (n + 1) ↾}_{\{\frac{n}{N}\}} = \{⟨\frac{n}{N}, Q (n + 1) (\frac{n}{N})⟩\}$
249	235 242 248	3eqtr4d	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n} Q (k) ↾}_{\{\frac{n}{N}\}} = {Q (n + 1) ↾}_{\{\frac{n}{N}\}}$
250		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
251		xrmaxle	$⊢ (0 \in ℝ^{} \land \frac{n}{N} \in ℝ^{} \land z \in ℝ^{*}) \to (if (0 \leq \frac{n}{N}, \frac{n}{N}, 0) \leq z \leftrightarrow (0 \leq z \land \frac{n}{N} \leq z))$
252		xrlemin	$⊢ (z \in ℝ^{} \land \frac{n}{N} \in ℝ^{} \land \frac{n + 1}{N} \in ℝ^{*}) \to (z \leq if (\frac{n}{N} \leq \frac{n + 1}{N}, \frac{n}{N}, \frac{n + 1}{N}) \leftrightarrow (z \leq \frac{n}{N} \land z \leq \frac{n + 1}{N}))$
253	250 251 252	ixxin	$⊢ ((0 \in ℝ^{} \land \frac{n}{N} \in ℝ^{}) \land (\frac{n}{N} \in ℝ^{} \land \frac{n + 1}{N} \in ℝ^{})) \to [0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}] = [if (0 \leq \frac{n}{N}, \frac{n}{N}, 0), if (\frac{n}{N} \leq \frac{n + 1}{N}, \frac{n}{N}, \frac{n + 1}{N})]$
254	238 208 208 244 253	syl22anc	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}] = [if (0 \leq \frac{n}{N}, \frac{n}{N}, 0), if (\frac{n}{N} \leq \frac{n + 1}{N}, \frac{n}{N}, \frac{n + 1}{N})]$
255	142	iftrued	$⊢ (φ \land χ) \to if (0 \leq \frac{n}{N}, \frac{n}{N}, 0) = \frac{n}{N}$
256	147	iftrued	$⊢ (φ \land χ) \to if (\frac{n}{N} \leq \frac{n + 1}{N}, \frac{n}{N}, \frac{n + 1}{N}) = \frac{n}{N}$
257	255 256	oveq12d	$⊢ (φ \land χ) \to [if (0 \leq \frac{n}{N}, \frac{n}{N}, 0), if (\frac{n}{N} \leq \frac{n + 1}{N}, \frac{n}{N}, \frac{n + 1}{N})] = [\frac{n}{N}, \frac{n}{N}]$
258		iccid	$⊢ \frac{n}{N} \in ℝ^{*} \to [\frac{n}{N}, \frac{n}{N}] = \{\frac{n}{N}\}$
259	208 258	syl	$⊢ (φ \land χ) \to [\frac{n}{N}, \frac{n}{N}] = \{\frac{n}{N}\}$
260	254 257 259	3eqtrd	$⊢ (φ \land χ) \to [0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}] = \{\frac{n}{N}\}$
261	260	reseq2d	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n} Q (k) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])} = {⋃_{k = 1}^{n} Q (k) ↾}_{\{\frac{n}{N}\}}$
262	260	reseq2d	$⊢ (φ \land χ) \to {Q (n + 1) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])} = {Q (n + 1) ↾}_{\{\frac{n}{N}\}}$
263	249 261 262	3eqtr4d	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n} Q (k) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])} = {Q (n + 1) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])}$
264		fresaun	$⊢ (⋃_{k = 1}^{n} Q (k) : [0, \frac{n}{N}] ⟶ B \land Q (n + 1) : [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B \land {⋃_{k = 1}^{n} Q (k) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])} = {Q (n + 1) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])}) \to (⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) : [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B$
265	182 196 263 264	syl3anc	$⊢ (φ \land χ) \to (⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) : [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B$
266		fzsuc	$⊢ n \in ℤ_{\geq 1} \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
267	198 266	syl	$⊢ (φ \land χ) \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
268	267	iuneq1d	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n + 1} Q (k) = ⋃_{k \in (1 \dots n) \cup \{n + 1\}} Q (k)$
269		iunxun	$⊢ ⋃_{k \in (1 \dots n) \cup \{n + 1\}} Q (k) = ⋃_{k = 1}^{n} Q (k) \cup ⋃_{k \in \{n + 1\}} Q (k)$
270		ovex	$⊢ n + 1 \in V$
271		fveq2	$⊢ k = n + 1 \to Q (k) = Q (n + 1)$
272	270 271	iunxsn	$⊢ ⋃_{k \in \{n + 1\}} Q (k) = Q (n + 1)$
273	272	uneq2i	$⊢ ⋃_{k = 1}^{n} Q (k) \cup ⋃_{k \in \{n + 1\}} Q (k) = ⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)$
274	269 273	eqtri	$⊢ ⋃_{k \in (1 \dots n) \cup \{n + 1\}} Q (k) = ⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)$
275	268 274	eqtr2di	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n} Q (k) \cup Q (n + 1) = ⋃_{k = 1}^{n + 1} Q (k)$
276	275	feq1d	$⊢ (φ \land χ) \to ((⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) : [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B \leftrightarrow ⋃_{k = 1}^{n + 1} Q (k) : [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B)$
277	265 276	mpbid	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n + 1} Q (k) : [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B$
278	170	feq2d	$⊢ (φ \land χ) \to (⋃_{k = 1}^{n + 1} Q (k) : [0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B \leftrightarrow ⋃_{k = 1}^{n + 1} Q (k) : ⋃ (L ↾_{𝑡} [0, \frac{n + 1}{N}]) ⟶ B)$
279	277 278	mpbid	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n + 1} Q (k) : ⋃ (L ↾_{𝑡} [0, \frac{n + 1}{N}]) ⟶ B$
280	275	reseq1d	$⊢ (φ \land χ) \to {(⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) ↾}_{[0, \frac{n}{N}]} = {⋃_{k = 1}^{n + 1} Q (k) ↾}_{[0, \frac{n}{N}]}$
281		fresaunres1	$⊢ (⋃_{k = 1}^{n} Q (k) : [0, \frac{n}{N}] ⟶ B \land Q (n + 1) : [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B \land {⋃_{k = 1}^{n} Q (k) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])} = {Q (n + 1) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])}) \to {(⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) ↾}_{[0, \frac{n}{N}]} = ⋃_{k = 1}^{n} Q (k)$
282	182 196 263 281	syl3anc	$⊢ (φ \land χ) \to {(⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) ↾}_{[0, \frac{n}{N}]} = ⋃_{k = 1}^{n} Q (k)$
283	280 282	eqtr3d	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n + 1} Q (k) ↾}_{[0, \frac{n}{N}]} = ⋃_{k = 1}^{n} Q (k)$
284	167	a1i	$⊢ (φ \land χ) \to L \in Top$
285		ovex	$⊢ [0, \frac{n + 1}{N}] \in V$
286	285	a1i	$⊢ (φ \land χ) \to [0, \frac{n + 1}{N}] \in V$
287		restabs	$⊢ (L \in Top \land [0, \frac{n}{N}] \subseteq [0, \frac{n + 1}{N}] \land [0, \frac{n + 1}{N}] \in V) \to (L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [0, \frac{n}{N}] = L ↾_{𝑡} [0, \frac{n}{N}]$
288	284 153 286 287	syl3anc	$⊢ (φ \land χ) \to (L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [0, \frac{n}{N}] = L ↾_{𝑡} [0, \frac{n}{N}]$
289	288	oveq1d	$⊢ (φ \land χ) \to ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [0, \frac{n}{N}]) Cn C = (L ↾_{𝑡} [0, \frac{n}{N}]) Cn C$
290	173 283 289	3eltr4d	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n + 1} Q (k) ↾}_{[0, \frac{n}{N}]} \in (((L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [0, \frac{n}{N}]) Cn C)$
291	1 2 3 4 5 6 7 8 9 10 11 12 183	cvmliftlem8	$⊢ (φ \land n + 1 \in (1 \dots N)) \to Q (n + 1) \in ((L ↾_{𝑡} [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]) Cn C)$
292	119 291	syldan	$⊢ (φ \land χ) \to Q (n + 1) \in ((L ↾_{𝑡} [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]) Cn C)$
293	194	oveq2d	$⊢ (φ \land χ) \to L ↾_{𝑡} [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}] = L ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]$
294	293	oveq1d	$⊢ (φ \land χ) \to (L ↾_{𝑡} [\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]) Cn C = (L ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]) Cn C$
295	292 294	eleqtrd	$⊢ (φ \land χ) \to Q (n + 1) \in ((L ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]) Cn C)$
296	275	reseq1d	$⊢ (φ \land χ) \to {(⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]} = {⋃_{k = 1}^{n + 1} Q (k) ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}$
297		fresaunres2	$⊢ (⋃_{k = 1}^{n} Q (k) : [0, \frac{n}{N}] ⟶ B \land Q (n + 1) : [\frac{n}{N}, \frac{n + 1}{N}] ⟶ B \land {⋃_{k = 1}^{n} Q (k) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])} = {Q (n + 1) ↾}_{([0, \frac{n}{N}] \cap [\frac{n}{N}, \frac{n + 1}{N}])}) \to {(⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]} = Q (n + 1)$
298	182 196 263 297	syl3anc	$⊢ (φ \land χ) \to {(⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]} = Q (n + 1)$
299	296 298	eqtr3d	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n + 1} Q (k) ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]} = Q (n + 1)$
300		restabs	$⊢ (L \in Top \land [\frac{n}{N}, \frac{n + 1}{N}] \subseteq [0, \frac{n + 1}{N}] \land [0, \frac{n + 1}{N}] \in V) \to (L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}] = L ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]$
301	284 163 286 300	syl3anc	$⊢ (φ \land χ) \to (L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}] = L ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]$
302	301	oveq1d	$⊢ (φ \land χ) \to ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]) Cn C = (L ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]) Cn C$
303	295 299 302	3eltr4d	$⊢ (φ \land χ) \to {⋃_{k = 1}^{n + 1} Q (k) ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]} \in (((L ↾_{𝑡} [0, \frac{n + 1}{N}]) ↾_{𝑡} [\frac{n}{N}, \frac{n + 1}{N}]) Cn C)$
304	115 2 158 165 170 279 290 303	paste	$⊢ (φ \land χ) \to ⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C)$
305	152	reseq2d	$⊢ (φ \land χ) \to {G ↾}_{[0, \frac{n + 1}{N}]} = {G ↾}_{([0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}])}$
306	172	simprd	$⊢ (φ \land χ) \to F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}$
307	187	simprd	$⊢ (φ \land χ) \to F \circ Q (n + 1) = {G ↾}_{[\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]}$
308	194	reseq2d	$⊢ (φ \land χ) \to {G ↾}_{[\frac{n + 1 - 1}{N}, \frac{n + 1}{N}]} = {G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}$
309	307 308	eqtrd	$⊢ (φ \land χ) \to F \circ Q (n + 1) = {G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]}$
310	306 309	uneq12d	$⊢ (φ \land χ) \to (F \circ ⋃_{k = 1}^{n} Q (k)) \cup (F \circ Q (n + 1)) = ({G ↾}_{[0, \frac{n}{N}]}) \cup ({G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]})$
311		coundi	$⊢ F \circ (⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) = (F \circ ⋃_{k = 1}^{n} Q (k)) \cup (F \circ Q (n + 1))$
312		resundi	$⊢ {G ↾}_{([0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}])} = ({G ↾}_{[0, \frac{n}{N}]}) \cup ({G ↾}_{[\frac{n}{N}, \frac{n + 1}{N}]})$
313	310 311 312	3eqtr4g	$⊢ (φ \land χ) \to F \circ (⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) = {G ↾}_{([0, \frac{n}{N}] \cup [\frac{n}{N}, \frac{n + 1}{N}])}$
314	275	coeq2d	$⊢ (φ \land χ) \to F \circ (⋃_{k = 1}^{n} Q (k) \cup Q (n + 1)) = F \circ ⋃_{k = 1}^{n + 1} Q (k)$
315	305 313 314	3eqtr2rd	$⊢ (φ \land χ) \to F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]}$
316	304 315	jca	$⊢ (φ \land χ) \to (⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]})$
317	14 316	sylan2br	$⊢ (φ \land ((n \in ℕ \land n + 1 \in (1 \dots N)) \land (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}))) \to (⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]})$
318	317	expr	$⊢ (φ \land (n \in ℕ \land n + 1 \in (1 \dots N))) \to ((⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}) \to (⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]}))$
319	114 318	animpimp2impd	$⊢ n \in ℕ \to ((φ \to (n \in (1 \dots N) \to (⋃_{k = 1}^{n} Q (k) \in ((L ↾_{𝑡} [0, \frac{n}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n} Q (k) = {G ↾}_{[0, \frac{n}{N}]}))) \to (φ \to (n + 1 \in (1 \dots N) \to (⋃_{k = 1}^{n + 1} Q (k) \in ((L ↾_{𝑡} [0, \frac{n + 1}{N}]) Cn C) \land F \circ ⋃_{k = 1}^{n + 1} Q (k) = {G ↾}_{[0, \frac{n + 1}{N}]}))))$
320	40 54 68 83 107 319	nnind	$⊢ N \in ℕ \to (φ \to (N \in (1 \dots N) \to (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{N}]})))$
321	8 320	mpcom	$⊢ φ \to (N \in (1 \dots N) \to (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{N}]}))$
322	18 321	mpd	$⊢ φ \to (K \in ((L ↾_{𝑡} [0, \frac{N}{N}]) Cn C) \land F \circ K = {G ↾}_{[0, \frac{N}{N}]})$

Metamath Proof Explorer

Theorem cvmliftlem10

Proof