cvmliftlem8

Description: Lemma for cvmlift . The functions Q are continuous functions because they are defined as ` ``' ( F |`I ) o. G where G is continuous and ` ( F |`I ) is a homeomorphism. (Contributed by Mario Carneiro, 16-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	cvmliftlem8	$⊢ (φ \land M \in (1 \dots N)) \to Q (M) \in ((L ↾_{𝑡} W) Cn C)$

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		elfznn	$⊢ M \in (1 \dots N) \to M \in ℕ$
15	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem5	$⊢ (φ \land M \in ℕ) \to Q (M) = (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z)))$
16	14 15	sylan2	$⊢ (φ \land M \in (1 \dots N)) \to Q (M) = (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z)))$
17	4	adantr	$⊢ (φ \land M \in (1 \dots N)) \to F \in (C CovMap J)$
18		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
19		cnrest2r	$⊢ C \in Top \to (L ↾_{𝑡} W) Cn (C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)) \subseteq (L ↾_{𝑡} W) Cn C$
20	17 18 19	3syl	$⊢ (φ \land M \in (1 \dots N)) \to (L ↾_{𝑡} W) Cn (C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)) \subseteq (L ↾_{𝑡} W) Cn C$
21		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
22	11 21	eqeltri	$⊢ L \in TopOn (ℝ)$
23		simpr	$⊢ (φ \land M \in (1 \dots N)) \to M \in (1 \dots N)$
24	1 2 3 4 5 6 7 8 9 10 11 23 13	cvmliftlem2	$⊢ (φ \land M \in (1 \dots N)) \to W \subseteq [0, 1]$
25		unitssre	$⊢ [0, 1] \subseteq ℝ$
26	24 25	sstrdi	$⊢ (φ \land M \in (1 \dots N)) \to W \subseteq ℝ$
27		resttopon	$⊢ (L \in TopOn (ℝ) \land W \subseteq ℝ) \to L ↾_{𝑡} W \in TopOn (W)$
28	22 26 27	sylancr	$⊢ (φ \land M \in (1 \dots N)) \to L ↾_{𝑡} W \in TopOn (W)$
29		eqid	$⊢ II ↾_{𝑡} W = II ↾_{𝑡} W$
30		iitopon	$⊢ II \in TopOn ([0, 1])$
31	30	a1i	$⊢ (φ \land M \in (1 \dots N)) \to II \in TopOn ([0, 1])$
32	5	adantr	$⊢ (φ \land M \in (1 \dots N)) \to G \in (II Cn J)$
33		iiuni	$⊢ [0, 1] = ⋃ II$
34	33 3	cnf	$⊢ G \in (II Cn J) \to G : [0, 1] ⟶ X$
35	32 34	syl	$⊢ (φ \land M \in (1 \dots N)) \to G : [0, 1] ⟶ X$
36	35	feqmptd	$⊢ (φ \land M \in (1 \dots N)) \to G = (z \in [0, 1] ⟼ G (z))$
37	36 32	eqeltrrd	$⊢ (φ \land M \in (1 \dots N)) \to (z \in [0, 1] ⟼ G (z)) \in (II Cn J)$
38	29 31 24 37	cnmpt1res	$⊢ (φ \land M \in (1 \dots N)) \to (z \in W ⟼ G (z)) \in ((II ↾_{𝑡} W) Cn J)$
39		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
40	11	oveq1i	$⊢ L ↾_{𝑡} [0, 1] = topGen (ran (.)) ↾_{𝑡} [0, 1]$
41	39 40	eqtr4i	$⊢ II = L ↾_{𝑡} [0, 1]$
42	41	oveq1i	$⊢ II ↾_{𝑡} W = (L ↾_{𝑡} [0, 1]) ↾_{𝑡} W$
43		retop	$⊢ topGen (ran (.)) \in Top$
44	11 43	eqeltri	$⊢ L \in Top$
45	44	a1i	$⊢ (φ \land M \in (1 \dots N)) \to L \in Top$
46		ovexd	$⊢ (φ \land M \in (1 \dots N)) \to [0, 1] \in V$
47		restabs	$⊢ (L \in Top \land W \subseteq [0, 1] \land [0, 1] \in V) \to (L ↾_{𝑡} [0, 1]) ↾_{𝑡} W = L ↾_{𝑡} W$
48	45 24 46 47	syl3anc	$⊢ (φ \land M \in (1 \dots N)) \to (L ↾_{𝑡} [0, 1]) ↾_{𝑡} W = L ↾_{𝑡} W$
49	42 48	eqtrid	$⊢ (φ \land M \in (1 \dots N)) \to II ↾_{𝑡} W = L ↾_{𝑡} W$
50	49	oveq1d	$⊢ (φ \land M \in (1 \dots N)) \to (II ↾_{𝑡} W) Cn J = (L ↾_{𝑡} W) Cn J$
51	38 50	eleqtrd	$⊢ (φ \land M \in (1 \dots N)) \to (z \in W ⟼ G (z)) \in ((L ↾_{𝑡} W) Cn J)$
52		cvmtop2	$⊢ F \in (C CovMap J) \to J \in Top$
53	17 52	syl	$⊢ (φ \land M \in (1 \dots N)) \to J \in Top$
54	3	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
55	53 54	sylib	$⊢ (φ \land M \in (1 \dots N)) \to J \in TopOn (X)$
56		simprl	$⊢ (φ \land (M \in (1 \dots N) \land z \in W)) \to M \in (1 \dots N)$
57		simprr	$⊢ (φ \land (M \in (1 \dots N) \land z \in W)) \to z \in W$
58	1 2 3 4 5 6 7 8 9 10 11 56 13 57	cvmliftlem3	$⊢ (φ \land (M \in (1 \dots N) \land z \in W)) \to G (z) \in 1^{st} (T (M))$
59	58	anassrs	$⊢ ((φ \land M \in (1 \dots N)) \land z \in W) \to G (z) \in 1^{st} (T (M))$
60	59	fmpttd	$⊢ (φ \land M \in (1 \dots N)) \to (z \in W ⟼ G (z)) : W ⟶ 1^{st} (T (M))$
61	60	frnd	$⊢ (φ \land M \in (1 \dots N)) \to ran (z \in W ⟼ G (z)) \subseteq 1^{st} (T (M))$
62	1 2 3 4 5 6 7 8 9 10 11 23	cvmliftlem1	$⊢ (φ \land M \in (1 \dots N)) \to 2^{nd} (T (M)) \in S (1^{st} (T (M)))$
63	1	cvmsrcl	$⊢ 2^{nd} (T (M)) \in S (1^{st} (T (M))) \to 1^{st} (T (M)) \in J$
64		elssuni	$⊢ 1^{st} (T (M)) \in J \to 1^{st} (T (M)) \subseteq ⋃ J$
65	62 63 64	3syl	$⊢ (φ \land M \in (1 \dots N)) \to 1^{st} (T (M)) \subseteq ⋃ J$
66	65 3	sseqtrrdi	$⊢ (φ \land M \in (1 \dots N)) \to 1^{st} (T (M)) \subseteq X$
67		cnrest2	$⊢ (J \in TopOn (X) \land ran (z \in W ⟼ G (z)) \subseteq 1^{st} (T (M)) \land 1^{st} (T (M)) \subseteq X) \to ((z \in W ⟼ G (z)) \in ((L ↾_{𝑡} W) Cn J) \leftrightarrow (z \in W ⟼ G (z)) \in ((L ↾_{𝑡} W) Cn (J ↾_{𝑡} 1^{st} (T (M)))))$
68	55 61 66 67	syl3anc	$⊢ (φ \land M \in (1 \dots N)) \to ((z \in W ⟼ G (z)) \in ((L ↾_{𝑡} W) Cn J) \leftrightarrow (z \in W ⟼ G (z)) \in ((L ↾_{𝑡} W) Cn (J ↾_{𝑡} 1^{st} (T (M)))))$
69	51 68	mpbid	$⊢ (φ \land M \in (1 \dots N)) \to (z \in W ⟼ G (z)) \in ((L ↾_{𝑡} W) Cn (J ↾_{𝑡} 1^{st} (T (M))))$
70	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem7	$⊢ (φ \land M \in (1 \dots N)) \to Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}]$
71		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
72	2 3	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ X$
73	17 71 72	3syl	$⊢ (φ \land M \in (1 \dots N)) \to F : B ⟶ X$
74		ffn	$⊢ F : B ⟶ X \to F Fn B$
75		fniniseg	$⊢ F Fn B \to (Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}] \leftrightarrow (Q (M - 1) (\frac{M - 1}{N}) \in B \land F (Q (M - 1) (\frac{M - 1}{N})) = G (\frac{M - 1}{N})))$
76	73 74 75	3syl	$⊢ (φ \land M \in (1 \dots N)) \to (Q (M - 1) (\frac{M - 1}{N}) \in F^{-1} [\{G (\frac{M - 1}{N})\}] \leftrightarrow (Q (M - 1) (\frac{M - 1}{N}) \in B \land F (Q (M - 1) (\frac{M - 1}{N})) = G (\frac{M - 1}{N})))$
77	70 76	mpbid	$⊢ (φ \land M \in (1 \dots N)) \to (Q (M - 1) (\frac{M - 1}{N}) \in B \land F (Q (M - 1) (\frac{M - 1}{N})) = G (\frac{M - 1}{N}))$
78	77	simpld	$⊢ (φ \land M \in (1 \dots N)) \to Q (M - 1) (\frac{M - 1}{N}) \in B$
79	77	simprd	$⊢ (φ \land M \in (1 \dots N)) \to F (Q (M - 1) (\frac{M - 1}{N})) = G (\frac{M - 1}{N})$
80	14	adantl	$⊢ (φ \land M \in (1 \dots N)) \to M \in ℕ$
81	80	nnred	$⊢ (φ \land M \in (1 \dots N)) \to M \in ℝ$
82		peano2rem	$⊢ M \in ℝ \to M - 1 \in ℝ$
83	81 82	syl	$⊢ (φ \land M \in (1 \dots N)) \to M - 1 \in ℝ$
84	8	adantr	$⊢ (φ \land M \in (1 \dots N)) \to N \in ℕ$
85	83 84	nndivred	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M - 1}{N} \in ℝ$
86	85	rexrd	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M - 1}{N} \in ℝ^{*}$
87	81 84	nndivred	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M}{N} \in ℝ$
88	87	rexrd	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M}{N} \in ℝ^{*}$
89	81	ltm1d	$⊢ (φ \land M \in (1 \dots N)) \to M - 1 < M$
90	84	nnred	$⊢ (φ \land M \in (1 \dots N)) \to N \in ℝ$
91	84	nngt0d	$⊢ (φ \land M \in (1 \dots N)) \to 0 < N$
92		ltdiv1	$⊢ (M - 1 \in ℝ \land M \in ℝ \land (N \in ℝ \land 0 < N)) \to (M - 1 < M \leftrightarrow \frac{M - 1}{N} < \frac{M}{N})$
93	83 81 90 91 92	syl112anc	$⊢ (φ \land M \in (1 \dots N)) \to (M - 1 < M \leftrightarrow \frac{M - 1}{N} < \frac{M}{N})$
94	89 93	mpbid	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M - 1}{N} < \frac{M}{N}$
95	85 87 94	ltled	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M - 1}{N} \leq \frac{M}{N}$
96		lbicc2	$⊢ (\frac{M - 1}{N} \in ℝ^{} \land \frac{M}{N} \in ℝ^{} \land \frac{M - 1}{N} \leq \frac{M}{N}) \to \frac{M - 1}{N} \in [\frac{M - 1}{N}, \frac{M}{N}]$
97	86 88 95 96	syl3anc	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M - 1}{N} \in [\frac{M - 1}{N}, \frac{M}{N}]$
98	97 13	eleqtrrdi	$⊢ (φ \land M \in (1 \dots N)) \to \frac{M - 1}{N} \in W$
99	1 2 3 4 5 6 7 8 9 10 11 23 13 98	cvmliftlem3	$⊢ (φ \land M \in (1 \dots N)) \to G (\frac{M - 1}{N}) \in 1^{st} (T (M))$
100	79 99	eqeltrd	$⊢ (φ \land M \in (1 \dots N)) \to F (Q (M - 1) (\frac{M - 1}{N})) \in 1^{st} (T (M))$
101		eqid	$⊢ (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b) = (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)$
102	1 2 101	cvmsiota	$⊢ (F \in (C CovMap J) \land (2^{nd} (T (M)) \in S (1^{st} (T (M))) \land Q (M - 1) (\frac{M - 1}{N}) \in B \land F (Q (M - 1) (\frac{M - 1}{N})) \in 1^{st} (T (M)))) \to ((ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b) \in 2^{nd} (T (M)) \land Q (M - 1) (\frac{M - 1}{N}) \in (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b))$
103	17 62 78 100 102	syl13anc	$⊢ (φ \land M \in (1 \dots N)) \to ((ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b) \in 2^{nd} (T (M)) \land Q (M - 1) (\frac{M - 1}{N}) \in (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b))$
104	103	simpld	$⊢ (φ \land M \in (1 \dots N)) \to (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b) \in 2^{nd} (T (M))$
105	1	cvmshmeo	$⊢ (2^{nd} (T (M)) \in S (1^{st} (T (M))) \land (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b) \in 2^{nd} (T (M))) \to {F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)} \in ((C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)) Homeo (J ↾_{𝑡} 1^{st} (T (M))))$
106	62 104 105	syl2anc	$⊢ (φ \land M \in (1 \dots N)) \to {F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)} \in ((C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)) Homeo (J ↾_{𝑡} 1^{st} (T (M))))$
107		hmeocnvcn	$⊢ {F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)} \in ((C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)) Homeo (J ↾_{𝑡} 1^{st} (T (M)))) \to {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} \in ((J ↾_{𝑡} 1^{st} (T (M))) Cn (C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)))$
108	106 107	syl	$⊢ (φ \land M \in (1 \dots N)) \to {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} \in ((J ↾_{𝑡} 1^{st} (T (M))) Cn (C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)))$
109	28 69 108	cnmpt11f	$⊢ (φ \land M \in (1 \dots N)) \to (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z))) \in ((L ↾_{𝑡} W) Cn (C ↾_{𝑡} (ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)))$
110	20 109	sseldd	$⊢ (φ \land M \in (1 \dots N)) \to (z \in W ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (M)) \| Q (M - 1) (\frac{M - 1}{N}) \in b)})}^{-1} (G (z))) \in ((L ↾_{𝑡} W) Cn C)$
111	16 110	eqeltrd	$⊢ (φ \land M \in (1 \dots N)) \to Q (M) \in ((L ↾_{𝑡} W) Cn C)$

Metamath Proof Explorer

Theorem cvmliftlem8

Proof