Metamath Proof Explorer


Theorem 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 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 cvmliftlem7 φ M 1 N Q M 1 M 1 N F -1 G M 1 N

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 fzssp1 0 N 1 0 N - 1 + 1
15 8 nncnd φ N
16 15 adantr φ M 1 N N
17 ax-1cn 1
18 npcan N 1 N - 1 + 1 = N
19 16 17 18 sylancl φ M 1 N N - 1 + 1 = N
20 19 oveq2d φ M 1 N 0 N - 1 + 1 = 0 N
21 14 20 sseqtrid φ M 1 N 0 N 1 0 N
22 simpr φ M 1 N M 1 N
23 elfzelz M 1 N M
24 8 nnzd φ N
25 elfzm1b M N M 1 N M 1 0 N 1
26 23 24 25 syl2anr φ M 1 N M 1 N M 1 0 N 1
27 22 26 mpbid φ M 1 N M 1 0 N 1
28 21 27 sseldd φ M 1 N M 1 0 N
29 elfznn0 M 1 0 N M 1 0
30 29 adantl φ M 1 0 N M 1 0
31 eleq1 y = 0 y 0 N 0 0 N
32 fveq2 y = 0 Q y = Q 0
33 oveq1 y = 0 y N = 0 N
34 32 33 fveq12d y = 0 Q y y N = Q 0 0 N
35 fvoveq1 y = 0 G y N = G 0 N
36 35 sneqd y = 0 G y N = G 0 N
37 36 imaeq2d y = 0 F -1 G y N = F -1 G 0 N
38 34 37 eleq12d y = 0 Q y y N F -1 G y N Q 0 0 N F -1 G 0 N
39 31 38 imbi12d y = 0 y 0 N Q y y N F -1 G y N 0 0 N Q 0 0 N F -1 G 0 N
40 39 imbi2d y = 0 φ y 0 N Q y y N F -1 G y N φ 0 0 N Q 0 0 N F -1 G 0 N
41 eleq1 y = n y 0 N n 0 N
42 fveq2 y = n Q y = Q n
43 oveq1 y = n y N = n N
44 42 43 fveq12d y = n Q y y N = Q n n N
45 fvoveq1 y = n G y N = G n N
46 45 sneqd y = n G y N = G n N
47 46 imaeq2d y = n F -1 G y N = F -1 G n N
48 44 47 eleq12d y = n Q y y N F -1 G y N Q n n N F -1 G n N
49 41 48 imbi12d y = n y 0 N Q y y N F -1 G y N n 0 N Q n n N F -1 G n N
50 49 imbi2d y = n φ y 0 N Q y y N F -1 G y N φ n 0 N Q n n N F -1 G n N
51 eleq1 y = n + 1 y 0 N n + 1 0 N
52 fveq2 y = n + 1 Q y = Q n + 1
53 oveq1 y = n + 1 y N = n + 1 N
54 52 53 fveq12d y = n + 1 Q y y N = Q n + 1 n + 1 N
55 fvoveq1 y = n + 1 G y N = G n + 1 N
56 55 sneqd y = n + 1 G y N = G n + 1 N
57 56 imaeq2d y = n + 1 F -1 G y N = F -1 G n + 1 N
58 54 57 eleq12d y = n + 1 Q y y N F -1 G y N Q n + 1 n + 1 N F -1 G n + 1 N
59 51 58 imbi12d y = n + 1 y 0 N Q y y N F -1 G y N n + 1 0 N Q n + 1 n + 1 N F -1 G n + 1 N
60 59 imbi2d y = n + 1 φ y 0 N Q y y N F -1 G y N φ n + 1 0 N Q n + 1 n + 1 N F -1 G n + 1 N
61 eleq1 y = M 1 y 0 N M 1 0 N
62 fveq2 y = M 1 Q y = Q M 1
63 oveq1 y = M 1 y N = M 1 N
64 62 63 fveq12d y = M 1 Q y y N = Q M 1 M 1 N
65 fvoveq1 y = M 1 G y N = G M 1 N
66 65 sneqd y = M 1 G y N = G M 1 N
67 66 imaeq2d y = M 1 F -1 G y N = F -1 G M 1 N
68 64 67 eleq12d y = M 1 Q y y N F -1 G y N Q M 1 M 1 N F -1 G M 1 N
69 61 68 imbi12d y = M 1 y 0 N Q y y N F -1 G y N M 1 0 N Q M 1 M 1 N F -1 G M 1 N
70 69 imbi2d y = M 1 φ y 0 N Q y y N F -1 G y N φ M 1 0 N Q M 1 M 1 N F -1 G M 1 N
71 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem4 Q 0 = 0 P
72 71 a1i φ Q 0 = 0 P
73 8 nnne0d φ N 0
74 15 73 div0d φ 0 N = 0
75 72 74 fveq12d φ Q 0 0 N = 0 P 0
76 0nn0 0 0
77 fvsng 0 0 P B 0 P 0 = P
78 76 6 77 sylancr φ 0 P 0 = P
79 75 78 eqtrd φ Q 0 0 N = P
80 74 fveq2d φ G 0 N = G 0
81 7 80 eqtr4d φ F P = G 0 N
82 cvmcn F C CovMap J F C Cn J
83 4 82 syl φ F C Cn J
84 2 3 cnf F C Cn J F : B X
85 ffn F : B X F Fn B
86 83 84 85 3syl φ F Fn B
87 fniniseg F Fn B P F -1 G 0 N P B F P = G 0 N
88 86 87 syl φ P F -1 G 0 N P B F P = G 0 N
89 6 81 88 mpbir2and φ P F -1 G 0 N
90 79 89 eqeltrd φ Q 0 0 N F -1 G 0 N
91 90 a1d φ 0 0 N Q 0 0 N F -1 G 0 N
92 id n 0 n 0
93 nn0uz 0 = 0
94 92 93 eleqtrdi n 0 n 0
95 94 adantl φ n 0 n 0
96 peano2fzr n 0 n + 1 0 N n 0 N
97 96 ex n 0 n + 1 0 N n 0 N
98 95 97 syl φ n 0 n + 1 0 N n 0 N
99 98 imim1d φ n 0 n 0 N Q n n N F -1 G n N n + 1 0 N Q n n N F -1 G n N
100 eqid n + 1 - 1 N n + 1 N = n + 1 - 1 N n + 1 N
101 simprlr φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 0 N
102 elfzle2 n + 1 0 N n + 1 N
103 101 102 syl φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 N
104 simprll φ n 0 n + 1 0 N Q n n N F -1 G n N n 0
105 nn0p1nn n 0 n + 1
106 104 105 syl φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1
107 nnuz = 1
108 106 107 eleqtrdi φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 1
109 24 adantr φ n 0 n + 1 0 N Q n n N F -1 G n N N
110 elfz5 n + 1 1 N n + 1 1 N n + 1 N
111 108 109 110 syl2anc φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 1 N n + 1 N
112 103 111 mpbird φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 1 N
113 simprr φ n 0 n + 1 0 N Q n n N F -1 G n N Q n n N F -1 G n N
114 104 nn0cnd φ n 0 n + 1 0 N Q n n N F -1 G n N n
115 pncan n 1 n + 1 - 1 = n
116 114 17 115 sylancl φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 - 1 = n
117 116 fveq2d φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 - 1 = Q n
118 116 oveq1d φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 - 1 N = n N
119 117 118 fveq12d φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 - 1 n + 1 - 1 N = Q n n N
120 118 fveq2d φ n 0 n + 1 0 N Q n n N F -1 G n N G n + 1 - 1 N = G n N
121 120 sneqd φ n 0 n + 1 0 N Q n n N F -1 G n N G n + 1 - 1 N = G n N
122 121 imaeq2d φ n 0 n + 1 0 N Q n n N F -1 G n N F -1 G n + 1 - 1 N = F -1 G n N
123 113 119 122 3eltr4d φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 - 1 n + 1 - 1 N F -1 G n + 1 - 1 N
124 1 2 3 4 5 6 7 8 9 10 11 12 100 112 123 cvmliftlem6 φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 : n + 1 - 1 N n + 1 N B F Q n + 1 = G n + 1 - 1 N n + 1 N
125 124 simpld φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 : n + 1 - 1 N n + 1 N B
126 104 nn0red φ n 0 n + 1 0 N Q n n N F -1 G n N n
127 8 adantr φ n 0 n + 1 0 N Q n n N F -1 G n N N
128 126 127 nndivred φ n 0 n + 1 0 N Q n n N F -1 G n N n N
129 128 rexrd φ n 0 n + 1 0 N Q n n N F -1 G n N n N *
130 peano2re n n + 1
131 126 130 syl φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1
132 131 127 nndivred φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 N
133 132 rexrd φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 N *
134 126 ltp1d φ n 0 n + 1 0 N Q n n N F -1 G n N n < n + 1
135 127 nnred φ n 0 n + 1 0 N Q n n N F -1 G n N N
136 127 nngt0d φ n 0 n + 1 0 N Q n n N F -1 G n N 0 < N
137 ltdiv1 n n + 1 N 0 < N n < n + 1 n N < n + 1 N
138 126 131 135 136 137 syl112anc φ n 0 n + 1 0 N Q n n N F -1 G n N n < n + 1 n N < n + 1 N
139 134 138 mpbid φ n 0 n + 1 0 N Q n n N F -1 G n N n N < n + 1 N
140 128 132 139 ltled φ n 0 n + 1 0 N Q n n N F -1 G n N n N n + 1 N
141 ubicc2 n N * n + 1 N * n N n + 1 N n + 1 N n N n + 1 N
142 129 133 140 141 syl3anc φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 N n N n + 1 N
143 118 oveq1d φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 - 1 N n + 1 N = n N n + 1 N
144 142 143 eleqtrrd φ n 0 n + 1 0 N Q n n N F -1 G n N n + 1 N n + 1 - 1 N n + 1 N
145 125 144 ffvelrnd φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 n + 1 N B
146 124 simprd φ n 0 n + 1 0 N Q n n N F -1 G n N F Q n + 1 = G n + 1 - 1 N n + 1 N
147 143 reseq2d φ n 0 n + 1 0 N Q n n N F -1 G n N G n + 1 - 1 N n + 1 N = G n N n + 1 N
148 146 147 eqtrd φ n 0 n + 1 0 N Q n n N F -1 G n N F Q n + 1 = G n N n + 1 N
149 148 fveq1d φ n 0 n + 1 0 N Q n n N F -1 G n N F Q n + 1 n + 1 N = G n N n + 1 N n + 1 N
150 143 feq2d φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 : n + 1 - 1 N n + 1 N B Q n + 1 : n N n + 1 N B
151 125 150 mpbid φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 : n N n + 1 N B
152 fvco3 Q n + 1 : n N n + 1 N B n + 1 N n N n + 1 N F Q n + 1 n + 1 N = F Q n + 1 n + 1 N
153 151 142 152 syl2anc φ n 0 n + 1 0 N Q n n N F -1 G n N F Q n + 1 n + 1 N = F Q n + 1 n + 1 N
154 fvres n + 1 N n N n + 1 N G n N n + 1 N n + 1 N = G n + 1 N
155 142 154 syl φ n 0 n + 1 0 N Q n n N F -1 G n N G n N n + 1 N n + 1 N = G n + 1 N
156 149 153 155 3eqtr3d φ n 0 n + 1 0 N Q n n N F -1 G n N F Q n + 1 n + 1 N = G n + 1 N
157 86 adantr φ n 0 n + 1 0 N Q n n N F -1 G n N F Fn B
158 fniniseg F Fn B Q n + 1 n + 1 N F -1 G n + 1 N Q n + 1 n + 1 N B F Q n + 1 n + 1 N = G n + 1 N
159 157 158 syl φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 n + 1 N F -1 G n + 1 N Q n + 1 n + 1 N B F Q n + 1 n + 1 N = G n + 1 N
160 145 156 159 mpbir2and φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 n + 1 N F -1 G n + 1 N
161 160 expr φ n 0 n + 1 0 N Q n n N F -1 G n N Q n + 1 n + 1 N F -1 G n + 1 N
162 99 161 animpimp2impd n 0 φ n 0 N Q n n N F -1 G n N φ n + 1 0 N Q n + 1 n + 1 N F -1 G n + 1 N
163 40 50 60 70 91 162 nn0ind M 1 0 φ M 1 0 N Q M 1 M 1 N F -1 G M 1 N
164 163 impd M 1 0 φ M 1 0 N Q M 1 M 1 N F -1 G M 1 N
165 30 164 mpcom φ M 1 0 N Q M 1 M 1 N F -1 G M 1 N
166 28 165 syldan φ M 1 N Q M 1 M 1 N F -1 G M 1 N