Metamath Proof Explorer

Theorem 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 ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
cvmliftlem.b ⊢ B = ⋃ C
cvmliftlem.x ⊢ X = ⋃ J
cvmliftlem.f ⊢ φ → F ∈ C CovMap J
cvmliftlem.g ⊢ φ → G ∈ II Cn J
cvmliftlem.p ⊢ φ → P ∈ B
cvmliftlem.e ⊢ φ → F ⁡ P = G ⁡ 0
cvmliftlem.n ⊢ φ → N ∈ ℕ
cvmliftlem.t ⊢ φ → T : 1 … N ⟶ ⋃ j ∈ J j × S ⁡ j
cvmliftlem.a ⊢ φ → ∀ k ∈ 1 … N G k − 1 N k N ⊆ 1 st ⁡ T ⁡ k
cvmliftlem.l ⊢ L = topGen ⁡ ran ⁡ .
cvmliftlem.q ⊢ Q = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P
cvmliftlem5.3 ⊢ W = M − 1 N M N
Assertion cvmliftlem8 ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M ∈ L ↾ 𝑡 W Cn C

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 ⊢ S = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
2 cvmliftlem.b ⊢ B = ⋃ C
3 cvmliftlem.x ⊢ X = ⋃ J
4 cvmliftlem.f ⊢ φ → F ∈ C CovMap J
5 cvmliftlem.g ⊢ φ → G ∈ II Cn J
6 cvmliftlem.p ⊢ φ → P ∈ B
7 cvmliftlem.e ⊢ φ → F ⁡ P = G ⁡ 0
8 cvmliftlem.n ⊢ φ → N ∈ ℕ
9 cvmliftlem.t ⊢ φ → T : 1 … N ⟶ ⋃ j ∈ J j × S ⁡ j
10 cvmliftlem.a ⊢ φ → ∀ k ∈ 1 … N G k − 1 N k N ⊆ 1 st ⁡ T ⁡ k
11 cvmliftlem.l ⊢ L = topGen ⁡ ran ⁡ .
12 cvmliftlem.q ⊢ Q = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P
13 cvmliftlem5.3 ⊢ W = M − 1 N M N
14 elfznn ⊢ M ∈ 1 … N → M ∈ ℕ
15 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem5 ⊢ φ ∧ M ∈ ℕ → Q ⁡ M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
16 14 15 sylan2 ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
17 4 adantr ⊢ φ ∧ M ∈ 1 … N → F ∈ C CovMap J
18 cvmtop1 ⊢ F ∈ C CovMap J → C ∈ Top
19 cnrest2r ⊢ C ∈ Top → L ↾ 𝑡 W Cn C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ⊆ L ↾ 𝑡 W Cn C
20 17 18 19 3syl ⊢ φ ∧ M ∈ 1 … N → L ↾ 𝑡 W Cn C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ⊆ L ↾ 𝑡 W Cn C
21 retopon ⊢ topGen ⁡ ran ⁡ . ∈ TopOn ⁡ ℝ
22 11 21 eqeltri ⊢ L ∈ TopOn ⁡ ℝ
23 simpr ⊢ φ ∧ M ∈ 1 … N → M ∈ 1 … N
24 1 2 3 4 5 6 7 8 9 10 11 23 13 cvmliftlem2 ⊢ φ ∧ M ∈ 1 … N → W ⊆ 0 1
25 unitssre ⊢ 0 1 ⊆ ℝ
26 24 25 sstrdi ⊢ φ ∧ M ∈ 1 … N → W ⊆ ℝ
27 resttopon ⊢ L ∈ TopOn ⁡ ℝ ∧ W ⊆ ℝ → L ↾ 𝑡 W ∈ TopOn ⁡ W
28 22 26 27 sylancr ⊢ φ ∧ M ∈ 1 … N → L ↾ 𝑡 W ∈ TopOn ⁡ W
29 eqid ⊢ II ↾ 𝑡 W = II ↾ 𝑡 W
30 iitopon ⊢ II ∈ TopOn ⁡ 0 1
31 30 a1i ⊢ φ ∧ M ∈ 1 … N → II ∈ TopOn ⁡ 0 1
32 5 adantr ⊢ φ ∧ M ∈ 1 … N → G ∈ II Cn J
33 iiuni ⊢ 0 1 = ⋃ II
34 33 3 cnf ⊢ G ∈ II Cn J → G : 0 1 ⟶ X
35 32 34 syl ⊢ φ ∧ M ∈ 1 … N → G : 0 1 ⟶ X
36 35 feqmptd ⊢ φ ∧ M ∈ 1 … N → G = z ∈ 0 1 ⟼ G ⁡ z
37 36 32 eqeltrrd ⊢ φ ∧ M ∈ 1 … N → z ∈ 0 1 ⟼ G ⁡ z ∈ II Cn J
38 29 31 24 37 cnmpt1res ⊢ φ ∧ M ∈ 1 … N → z ∈ W ⟼ G ⁡ z ∈ 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 ⁡ . ∈ Top
44 11 43 eqeltri ⊢ L ∈ Top
45 44 a1i ⊢ φ ∧ M ∈ 1 … N → L ∈ Top
46 ovexd ⊢ φ ∧ M ∈ 1 … N → 0 1 ∈ V
47 restabs ⊢ L ∈ Top ∧ W ⊆ 0 1 ∧ 0 1 ∈ V → L ↾ 𝑡 0 1 ↾ 𝑡 W = L ↾ 𝑡 W
48 45 24 46 47 syl3anc ⊢ φ ∧ M ∈ 1 … N → L ↾ 𝑡 0 1 ↾ 𝑡 W = L ↾ 𝑡 W
49 42 48 eqtrid ⊢ φ ∧ M ∈ 1 … N → II ↾ 𝑡 W = L ↾ 𝑡 W
50 49 oveq1d ⊢ φ ∧ M ∈ 1 … N → II ↾ 𝑡 W Cn J = L ↾ 𝑡 W Cn J
51 38 50 eleqtrd ⊢ φ ∧ M ∈ 1 … N → z ∈ W ⟼ G ⁡ z ∈ L ↾ 𝑡 W Cn J
52 cvmtop2 ⊢ F ∈ C CovMap J → J ∈ Top
53 17 52 syl ⊢ φ ∧ M ∈ 1 … N → J ∈ Top
54 3 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
55 53 54 sylib ⊢ φ ∧ M ∈ 1 … N → J ∈ TopOn ⁡ X
56 simprl ⊢ φ ∧ M ∈ 1 … N ∧ z ∈ W → M ∈ 1 … N
57 simprr ⊢ φ ∧ M ∈ 1 … N ∧ z ∈ W → z ∈ W
58 1 2 3 4 5 6 7 8 9 10 11 56 13 57 cvmliftlem3 ⊢ φ ∧ M ∈ 1 … N ∧ z ∈ W → G ⁡ z ∈ 1 st ⁡ T ⁡ M
59 58 anassrs ⊢ φ ∧ M ∈ 1 … N ∧ z ∈ W → G ⁡ z ∈ 1 st ⁡ T ⁡ M
60 59 fmpttd ⊢ φ ∧ M ∈ 1 … N → z ∈ W ⟼ G ⁡ z : W ⟶ 1 st ⁡ T ⁡ M
61 60 frnd ⊢ φ ∧ M ∈ 1 … N → ran ⁡ z ∈ W ⟼ G ⁡ z ⊆ 1 st ⁡ T ⁡ M
62 1 2 3 4 5 6 7 8 9 10 11 23 cvmliftlem1 ⊢ φ ∧ M ∈ 1 … N → 2 nd ⁡ T ⁡ M ∈ S ⁡ 1 st ⁡ T ⁡ M
63 1 cvmsrcl ⊢ 2 nd ⁡ T ⁡ M ∈ S ⁡ 1 st ⁡ T ⁡ M → 1 st ⁡ T ⁡ M ∈ J
64 elssuni ⊢ 1 st ⁡ T ⁡ M ∈ J → 1 st ⁡ T ⁡ M ⊆ ⋃ J
65 62 63 64 3syl ⊢ φ ∧ M ∈ 1 … N → 1 st ⁡ T ⁡ M ⊆ ⋃ J
66 65 3 sseqtrrdi ⊢ φ ∧ M ∈ 1 … N → 1 st ⁡ T ⁡ M ⊆ X
67 cnrest2 ⊢ J ∈ TopOn ⁡ X ∧ ran ⁡ z ∈ W ⟼ G ⁡ z ⊆ 1 st ⁡ T ⁡ M ∧ 1 st ⁡ T ⁡ M ⊆ X → z ∈ W ⟼ G ⁡ z ∈ L ↾ 𝑡 W Cn J ↔ z ∈ W ⟼ G ⁡ z ∈ L ↾ 𝑡 W Cn J ↾ 𝑡 1 st ⁡ T ⁡ M
68 55 61 66 67 syl3anc ⊢ φ ∧ M ∈ 1 … N → z ∈ W ⟼ G ⁡ z ∈ L ↾ 𝑡 W Cn J ↔ z ∈ W ⟼ G ⁡ z ∈ L ↾ 𝑡 W Cn J ↾ 𝑡 1 st ⁡ T ⁡ M
69 51 68 mpbid ⊢ φ ∧ M ∈ 1 … N → z ∈ W ⟼ G ⁡ z ∈ L ↾ 𝑡 W Cn J ↾ 𝑡 1 st ⁡ T ⁡ M
70 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem7 ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M − 1 ⁡ M − 1 N ∈ F -1 G ⁡ M − 1 N
71 cvmcn ⊢ F ∈ C CovMap J → F ∈ C Cn J
72 2 3 cnf ⊢ F ∈ C Cn J → F : B ⟶ X
73 17 71 72 3syl ⊢ φ ∧ M ∈ 1 … N → F : B ⟶ X
74 ffn ⊢ F : B ⟶ X → F Fn B
75 fniniseg ⊢ F Fn B → Q ⁡ M − 1 ⁡ M − 1 N ∈ F -1 G ⁡ M − 1 N ↔ Q ⁡ M − 1 ⁡ M − 1 N ∈ B ∧ F ⁡ Q ⁡ M − 1 ⁡ M − 1 N = G ⁡ M − 1 N
76 73 74 75 3syl ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M − 1 ⁡ M − 1 N ∈ F -1 G ⁡ M − 1 N ↔ Q ⁡ M − 1 ⁡ M − 1 N ∈ B ∧ F ⁡ Q ⁡ M − 1 ⁡ M − 1 N = G ⁡ M − 1 N
77 70 76 mpbid ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M − 1 ⁡ M − 1 N ∈ B ∧ F ⁡ Q ⁡ M − 1 ⁡ M − 1 N = G ⁡ M − 1 N
78 77 simpld ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M − 1 ⁡ M − 1 N ∈ B
79 77 simprd ⊢ φ ∧ M ∈ 1 … N → F ⁡ Q ⁡ M − 1 ⁡ M − 1 N = G ⁡ M − 1 N
80 14 adantl ⊢ φ ∧ M ∈ 1 … N → M ∈ ℕ
81 80 nnred ⊢ φ ∧ M ∈ 1 … N → M ∈ ℝ
82 peano2rem ⊢ M ∈ ℝ → M − 1 ∈ ℝ
83 81 82 syl ⊢ φ ∧ M ∈ 1 … N → M − 1 ∈ ℝ
84 8 adantr ⊢ φ ∧ M ∈ 1 … N → N ∈ ℕ
85 83 84 nndivred ⊢ φ ∧ M ∈ 1 … N → M − 1 N ∈ ℝ
86 85 rexrd ⊢ φ ∧ M ∈ 1 … N → M − 1 N ∈ ℝ *
87 81 84 nndivred ⊢ φ ∧ M ∈ 1 … N → M N ∈ ℝ
88 87 rexrd ⊢ φ ∧ M ∈ 1 … N → M N ∈ ℝ *
89 81 ltm1d ⊢ φ ∧ M ∈ 1 … N → M − 1 < M
90 84 nnred ⊢ φ ∧ M ∈ 1 … N → N ∈ ℝ
91 84 nngt0d ⊢ φ ∧ M ∈ 1 … N → 0 < N
92 ltdiv1 ⊢ M − 1 ∈ ℝ ∧ M ∈ ℝ ∧ N ∈ ℝ ∧ 0 < N → M − 1 < M ↔ M − 1 N < M N
93 83 81 90 91 92 syl112anc ⊢ φ ∧ M ∈ 1 … N → M − 1 < M ↔ M − 1 N < M N
94 89 93 mpbid ⊢ φ ∧ M ∈ 1 … N → M − 1 N < M N
95 85 87 94 ltled ⊢ φ ∧ M ∈ 1 … N → M − 1 N ≤ M N
96 lbicc2 ⊢ M − 1 N ∈ ℝ * ∧ M N ∈ ℝ * ∧ M − 1 N ≤ M N → M − 1 N ∈ M − 1 N M N
97 86 88 95 96 syl3anc ⊢ φ ∧ M ∈ 1 … N → M − 1 N ∈ M − 1 N M N
98 97 13 eleqtrrdi ⊢ φ ∧ M ∈ 1 … N → M − 1 N ∈ W
99 1 2 3 4 5 6 7 8 9 10 11 23 13 98 cvmliftlem3 ⊢ φ ∧ M ∈ 1 … N → G ⁡ M − 1 N ∈ 1 st ⁡ T ⁡ M
100 79 99 eqeltrd ⊢ φ ∧ M ∈ 1 … N → F ⁡ Q ⁡ M − 1 ⁡ M − 1 N ∈ 1 st ⁡ T ⁡ M
101 eqid ⊢ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b = ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
102 1 2 101 cvmsiota ⊢ F ∈ C CovMap J ∧ 2 nd ⁡ T ⁡ M ∈ S ⁡ 1 st ⁡ T ⁡ M ∧ Q ⁡ M − 1 ⁡ M − 1 N ∈ B ∧ F ⁡ Q ⁡ M − 1 ⁡ M − 1 N ∈ 1 st ⁡ T ⁡ M → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ 2 nd ⁡ T ⁡ M ∧ Q ⁡ M − 1 ⁡ M − 1 N ∈ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
103 17 62 78 100 102 syl13anc ⊢ φ ∧ M ∈ 1 … N → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ 2 nd ⁡ T ⁡ M ∧ Q ⁡ M − 1 ⁡ M − 1 N ∈ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
104 103 simpld ⊢ φ ∧ M ∈ 1 … N → ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ 2 nd ⁡ T ⁡ M
105 1 cvmshmeo ⊢ 2 nd ⁡ T ⁡ M ∈ S ⁡ 1 st ⁡ T ⁡ M ∧ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ 2 nd ⁡ T ⁡ M → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b Homeo J ↾ 𝑡 1 st ⁡ T ⁡ M
106 62 104 105 syl2anc ⊢ φ ∧ M ∈ 1 … N → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b Homeo J ↾ 𝑡 1 st ⁡ T ⁡ M
107 hmeocnvcn ⊢ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b ∈ C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b Homeo J ↾ 𝑡 1 st ⁡ T ⁡ M → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ∈ J ↾ 𝑡 1 st ⁡ T ⁡ M Cn C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
108 106 107 syl ⊢ φ ∧ M ∈ 1 … N → F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ∈ J ↾ 𝑡 1 st ⁡ T ⁡ M Cn C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
109 28 69 108 cnmpt11f ⊢ φ ∧ M ∈ 1 … N → z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z ∈ L ↾ 𝑡 W Cn C ↾ 𝑡 ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
110 20 109 sseldd ⊢ φ ∧ M ∈ 1 … N → z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z ∈ L ↾ 𝑡 W Cn C
111 16 110 eqeltrd ⊢ φ ∧ M ∈ 1 … N → Q ⁡ M ∈ L ↾ 𝑡 W Cn C