Metamath Proof Explorer


Theorem uniioombllem4

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 φ F : 2
uniioombl.2 φ Disj x . F x
uniioombl.3 S = seq 1 + abs F
uniioombl.a A = ran . F
uniioombl.e φ vol * E
uniioombl.c φ C +
uniioombl.g φ G : 2
uniioombl.s φ E ran . G
uniioombl.t T = seq 1 + abs G
uniioombl.v φ sup ran T * < vol * E + C
uniioombl.m φ M
uniioombl.m2 φ T M sup ran T * < < C
uniioombl.k K = . G 1 M
uniioombl.n φ N
uniioombl.n2 φ j 1 M i = 1 N vol * . F i . G j vol * . G j A < C M
uniioombl.l L = . F 1 N
Assertion uniioombllem4 φ vol * K A vol * K L + C

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 uniioombl.2 φ Disj x . F x
3 uniioombl.3 S = seq 1 + abs F
4 uniioombl.a A = ran . F
5 uniioombl.e φ vol * E
6 uniioombl.c φ C +
7 uniioombl.g φ G : 2
8 uniioombl.s φ E ran . G
9 uniioombl.t T = seq 1 + abs G
10 uniioombl.v φ sup ran T * < vol * E + C
11 uniioombl.m φ M
12 uniioombl.m2 φ T M sup ran T * < < C
13 uniioombl.k K = . G 1 M
14 uniioombl.n φ N
15 uniioombl.n2 φ j 1 M i = 1 N vol * . F i . G j vol * . G j A < C M
16 uniioombl.l L = . F 1 N
17 inss1 K A K
18 imassrn . G 1 M ran . G
19 18 unissi . G 1 M ran . G
20 13 19 eqsstri K ran . G
21 7 uniiccdif φ ran . G ran . G vol * ran . G ran . G = 0
22 21 simpld φ ran . G ran . G
23 ovolficcss G : 2 ran . G
24 7 23 syl φ ran . G
25 22 24 sstrd φ ran . G
26 20 25 sstrid φ K
27 1 2 3 4 5 6 7 8 9 10 uniioombllem1 φ sup ran T * <
28 ssid ran . G ran . G
29 9 ovollb G : 2 ran . G ran . G vol * ran . G sup ran T * <
30 7 28 29 sylancl φ vol * ran . G sup ran T * <
31 ovollecl ran . G sup ran T * < vol * ran . G sup ran T * < vol * ran . G
32 25 27 30 31 syl3anc φ vol * ran . G
33 ovolsscl K ran . G ran . G vol * ran . G vol * K
34 20 25 32 33 mp3an2i φ vol * K
35 ovolsscl K A K K vol * K vol * K A
36 17 26 34 35 mp3an2i φ vol * K A
37 inss1 K L K
38 ovolsscl K L K K vol * K vol * K L
39 37 26 34 38 mp3an2i φ vol * K L
40 ssun2 j = 1 M i N + 1 . F i . G j K L j = 1 M i N + 1 . F i . G j
41 nnuz = 1
42 14 peano2nnd φ N + 1
43 42 41 eleqtrdi φ N + 1 1
44 uzsplit N + 1 1 1 = 1 N + 1 - 1 N + 1
45 43 44 syl φ 1 = 1 N + 1 - 1 N + 1
46 41 45 syl5eq φ = 1 N + 1 - 1 N + 1
47 14 nncnd φ N
48 ax-1cn 1
49 pncan N 1 N + 1 - 1 = N
50 47 48 49 sylancl φ N + 1 - 1 = N
51 50 oveq2d φ 1 N + 1 - 1 = 1 N
52 51 uneq1d φ 1 N + 1 - 1 N + 1 = 1 N N + 1
53 46 52 eqtrd φ = 1 N N + 1
54 53 iuneq1d φ i . F i = i 1 N N + 1 . F i
55 iunxun i 1 N N + 1 . F i = i = 1 N . F i i N + 1 . F i
56 54 55 eqtrdi φ i . F i = i = 1 N . F i i N + 1 . F i
57 ioof . : * × * 𝒫
58 inss2 2 2
59 rexpssxrxp 2 * × *
60 58 59 sstri 2 * × *
61 fss F : 2 2 * × * F : * × *
62 1 60 61 sylancl φ F : * × *
63 fco . : * × * 𝒫 F : * × * . F : 𝒫
64 57 62 63 sylancr φ . F : 𝒫
65 ffn . F : 𝒫 . F Fn
66 fniunfv . F Fn i . F i = ran . F
67 64 65 66 3syl φ i . F i = ran . F
68 fvco3 F : 2 i . F i = . F i
69 1 68 sylan φ i . F i = . F i
70 69 iuneq2dv φ i . F i = i . F i
71 67 70 eqtr3d φ ran . F = i . F i
72 4 71 syl5eq φ A = i . F i
73 ffun . F : 𝒫 Fun . F
74 funiunfv Fun . F i = 1 N . F i = . F 1 N
75 64 73 74 3syl φ i = 1 N . F i = . F 1 N
76 elfznn i 1 N i
77 1 76 68 syl2an φ i 1 N . F i = . F i
78 77 iuneq2dv φ i = 1 N . F i = i = 1 N . F i
79 75 78 eqtr3d φ . F 1 N = i = 1 N . F i
80 16 79 syl5eq φ L = i = 1 N . F i
81 80 uneq1d φ L i N + 1 . F i = i = 1 N . F i i N + 1 . F i
82 56 72 81 3eqtr4d φ A = L i N + 1 . F i
83 82 ineq2d φ K A = K L i N + 1 . F i
84 indi K L i N + 1 . F i = K L K i N + 1 . F i
85 83 84 eqtrdi φ K A = K L K i N + 1 . F i
86 fss G : 2 2 * × * G : * × *
87 7 60 86 sylancl φ G : * × *
88 fco . : * × * 𝒫 G : * × * . G : 𝒫
89 57 87 88 sylancr φ . G : 𝒫
90 ffun . G : 𝒫 Fun . G
91 funiunfv Fun . G j = 1 M . G j = . G 1 M
92 89 90 91 3syl φ j = 1 M . G j = . G 1 M
93 elfznn j 1 M j
94 fvco3 G : 2 j . G j = . G j
95 7 93 94 syl2an φ j 1 M . G j = . G j
96 95 iuneq2dv φ j = 1 M . G j = j = 1 M . G j
97 92 96 eqtr3d φ . G 1 M = j = 1 M . G j
98 13 97 syl5eq φ K = j = 1 M . G j
99 98 ineq2d φ i N + 1 . F i K = i N + 1 . F i j = 1 M . G j
100 incom K i N + 1 . F i = i N + 1 . F i K
101 iunin2 i N + 1 . G j . F i = . G j i N + 1 . F i
102 incom . F i . G j = . G j . F i
103 102 a1i i N + 1 . F i . G j = . G j . F i
104 103 iuneq2i i N + 1 . F i . G j = i N + 1 . G j . F i
105 incom i N + 1 . F i . G j = . G j i N + 1 . F i
106 101 104 105 3eqtr4ri i N + 1 . F i . G j = i N + 1 . F i . G j
107 106 a1i j 1 M i N + 1 . F i . G j = i N + 1 . F i . G j
108 107 iuneq2i j = 1 M i N + 1 . F i . G j = j = 1 M i N + 1 . F i . G j
109 iunin2 j = 1 M i N + 1 . F i . G j = i N + 1 . F i j = 1 M . G j
110 108 109 eqtr3i j = 1 M i N + 1 . F i . G j = i N + 1 . F i j = 1 M . G j
111 99 100 110 3eqtr4g φ K i N + 1 . F i = j = 1 M i N + 1 . F i . G j
112 111 uneq2d φ K L K i N + 1 . F i = K L j = 1 M i N + 1 . F i . G j
113 85 112 eqtrd φ K A = K L j = 1 M i N + 1 . F i . G j
114 40 113 sseqtrrid φ j = 1 M i N + 1 . F i . G j K A
115 114 17 sstrdi φ j = 1 M i N + 1 . F i . G j K
116 ovolsscl j = 1 M i N + 1 . F i . G j K K vol * K vol * j = 1 M i N + 1 . F i . G j
117 115 26 34 116 syl3anc φ vol * j = 1 M i N + 1 . F i . G j
118 39 117 readdcld φ vol * K L + vol * j = 1 M i N + 1 . F i . G j
119 6 rpred φ C
120 39 119 readdcld φ vol * K L + C
121 113 fveq2d φ vol * K A = vol * K L j = 1 M i N + 1 . F i . G j
122 37 26 sstrid φ K L
123 115 26 sstrd φ j = 1 M i N + 1 . F i . G j
124 ovolun K L vol * K L j = 1 M i N + 1 . F i . G j vol * j = 1 M i N + 1 . F i . G j vol * K L j = 1 M i N + 1 . F i . G j vol * K L + vol * j = 1 M i N + 1 . F i . G j
125 122 39 123 117 124 syl22anc φ vol * K L j = 1 M i N + 1 . F i . G j vol * K L + vol * j = 1 M i N + 1 . F i . G j
126 121 125 eqbrtrd φ vol * K A vol * K L + vol * j = 1 M i N + 1 . F i . G j
127 fzfid φ 1 M Fin
128 iunss j = 1 M i N + 1 . F i . G j K j 1 M i N + 1 . F i . G j K
129 115 128 sylib φ j 1 M i N + 1 . F i . G j K
130 129 r19.21bi φ j 1 M i N + 1 . F i . G j K
131 26 adantr φ j 1 M K
132 34 adantr φ j 1 M vol * K
133 ovolsscl i N + 1 . F i . G j K K vol * K vol * i N + 1 . F i . G j
134 130 131 132 133 syl3anc φ j 1 M vol * i N + 1 . F i . G j
135 127 134 fsumrecl φ j = 1 M vol * i N + 1 . F i . G j
136 130 131 sstrd φ j 1 M i N + 1 . F i . G j
137 136 134 jca φ j 1 M i N + 1 . F i . G j vol * i N + 1 . F i . G j
138 137 ralrimiva φ j 1 M i N + 1 . F i . G j vol * i N + 1 . F i . G j
139 ovolfiniun 1 M Fin j 1 M i N + 1 . F i . G j vol * i N + 1 . F i . G j vol * j = 1 M i N + 1 . F i . G j j = 1 M vol * i N + 1 . F i . G j
140 127 138 139 syl2anc φ vol * j = 1 M i N + 1 . F i . G j j = 1 M vol * i N + 1 . F i . G j
141 119 11 nndivred φ C M
142 141 adantr φ j 1 M C M
143 80 ineq2d φ . G j L = . G j i = 1 N . F i
144 143 adantr φ j 1 M . G j L = . G j i = 1 N . F i
145 102 a1i i 1 N . F i . G j = . G j . F i
146 145 iuneq2i i = 1 N . F i . G j = i = 1 N . G j . F i
147 iunin2 i = 1 N . G j . F i = . G j i = 1 N . F i
148 146 147 eqtri i = 1 N . F i . G j = . G j i = 1 N . F i
149 144 148 eqtr4di φ j 1 M . G j L = i = 1 N . F i . G j
150 fzfid φ j 1 M 1 N Fin
151 ffvelrn F : 2 i F i 2
152 1 76 151 syl2an φ i 1 N F i 2
153 152 elin2d φ i 1 N F i 2
154 1st2nd2 F i 2 F i = 1 st F i 2 nd F i
155 153 154 syl φ i 1 N F i = 1 st F i 2 nd F i
156 155 fveq2d φ i 1 N . F i = . 1 st F i 2 nd F i
157 df-ov 1 st F i 2 nd F i = . 1 st F i 2 nd F i
158 156 157 eqtr4di φ i 1 N . F i = 1 st F i 2 nd F i
159 ioombl 1 st F i 2 nd F i dom vol
160 158 159 eqeltrdi φ i 1 N . F i dom vol
161 160 adantlr φ j 1 M i 1 N . F i dom vol
162 ffvelrn G : 2 j G j 2
163 7 93 162 syl2an φ j 1 M G j 2
164 163 elin2d φ j 1 M G j 2
165 1st2nd2 G j 2 G j = 1 st G j 2 nd G j
166 164 165 syl φ j 1 M G j = 1 st G j 2 nd G j
167 166 fveq2d φ j 1 M . G j = . 1 st G j 2 nd G j
168 df-ov 1 st G j 2 nd G j = . 1 st G j 2 nd G j
169 167 168 eqtr4di φ j 1 M . G j = 1 st G j 2 nd G j
170 ioombl 1 st G j 2 nd G j dom vol
171 169 170 eqeltrdi φ j 1 M . G j dom vol
172 171 adantr φ j 1 M i 1 N . G j dom vol
173 inmbl . F i dom vol . G j dom vol . F i . G j dom vol
174 161 172 173 syl2anc φ j 1 M i 1 N . F i . G j dom vol
175 174 ralrimiva φ j 1 M i 1 N . F i . G j dom vol
176 finiunmbl 1 N Fin i 1 N . F i . G j dom vol i = 1 N . F i . G j dom vol
177 150 175 176 syl2anc φ j 1 M i = 1 N . F i . G j dom vol
178 149 177 eqeltrd φ j 1 M . G j L dom vol
179 inss2 . G j A A
180 1 uniiccdif φ ran . F ran . F vol * ran . F ran . F = 0
181 180 simpld φ ran . F ran . F
182 ovolficcss F : 2 ran . F
183 1 182 syl φ ran . F
184 181 183 sstrd φ ran . F
185 4 184 eqsstrid φ A
186 185 adantr φ j 1 M A
187 179 186 sstrid φ j 1 M . G j A
188 inss1 . G j A . G j
189 ioossre 1 st G j 2 nd G j
190 169 189 eqsstrdi φ j 1 M . G j
191 169 fveq2d φ j 1 M vol * . G j = vol * 1 st G j 2 nd G j
192 ovolfcl G : 2 j 1 st G j 2 nd G j 1 st G j 2 nd G j
193 7 93 192 syl2an φ j 1 M 1 st G j 2 nd G j 1 st G j 2 nd G j
194 ovolioo 1 st G j 2 nd G j 1 st G j 2 nd G j vol * 1 st G j 2 nd G j = 2 nd G j 1 st G j
195 193 194 syl φ j 1 M vol * 1 st G j 2 nd G j = 2 nd G j 1 st G j
196 191 195 eqtrd φ j 1 M vol * . G j = 2 nd G j 1 st G j
197 193 simp2d φ j 1 M 2 nd G j
198 193 simp1d φ j 1 M 1 st G j
199 197 198 resubcld φ j 1 M 2 nd G j 1 st G j
200 196 199 eqeltrd φ j 1 M vol * . G j
201 ovolsscl . G j A . G j . G j vol * . G j vol * . G j A
202 188 190 200 201 mp3an2i φ j 1 M vol * . G j A
203 mblsplit . G j L dom vol . G j A vol * . G j A vol * . G j A = vol * . G j A . G j L + vol * . G j A . G j L
204 178 187 202 203 syl3anc φ j 1 M vol * . G j A = vol * . G j A . G j L + vol * . G j A . G j L
205 imassrn . F 1 N ran . F
206 205 unissi . F 1 N ran . F
207 206 16 4 3sstr4i L A
208 sslin L A . G j L . G j A
209 207 208 mp1i φ j 1 M . G j L . G j A
210 sseqin2 . G j L . G j A . G j A . G j L = . G j L
211 209 210 sylib φ j 1 M . G j A . G j L = . G j L
212 211 fveq2d φ j 1 M vol * . G j A . G j L = vol * . G j L
213 indifdir A L . G j = A . G j L . G j
214 incom A . G j = . G j A
215 incom L . G j = . G j L
216 214 215 difeq12i A . G j L . G j = . G j A . G j L
217 213 216 eqtri A L . G j = . G j A . G j L
218 82 eqcomd φ L i N + 1 . F i = A
219 80 ineq1d φ L i N + 1 . F i = i = 1 N . F i i N + 1 . F i
220 2fveq3 x = i . F x = . F i
221 220 cbvdisjv Disj x . F x Disj i . F i
222 2 221 sylib φ Disj i . F i
223 fz1ssnn 1 N
224 223 a1i φ 1 N
225 uzss N + 1 1 N + 1 1
226 43 225 syl φ N + 1 1
227 226 41 sseqtrrdi φ N + 1
228 51 ineq1d φ 1 N + 1 - 1 N + 1 = 1 N N + 1
229 uzdisj 1 N + 1 - 1 N + 1 =
230 228 229 eqtr3di φ 1 N N + 1 =
231 disjiun Disj i . F i 1 N N + 1 1 N N + 1 = i = 1 N . F i i N + 1 . F i =
232 222 224 227 230 231 syl13anc φ i = 1 N . F i i N + 1 . F i =
233 219 232 eqtrd φ L i N + 1 . F i =
234 uneqdifeq L A L i N + 1 . F i = L i N + 1 . F i = A A L = i N + 1 . F i
235 207 233 234 sylancr φ L i N + 1 . F i = A A L = i N + 1 . F i
236 218 235 mpbid φ A L = i N + 1 . F i
237 236 adantr φ j 1 M A L = i N + 1 . F i
238 237 ineq2d φ j 1 M . G j A L = . G j i N + 1 . F i
239 incom A L . G j = . G j A L
240 104 101 eqtri i N + 1 . F i . G j = . G j i N + 1 . F i
241 238 239 240 3eqtr4g φ j 1 M A L . G j = i N + 1 . F i . G j
242 217 241 eqtr3id φ j 1 M . G j A . G j L = i N + 1 . F i . G j
243 242 fveq2d φ j 1 M vol * . G j A . G j L = vol * i N + 1 . F i . G j
244 212 243 oveq12d φ j 1 M vol * . G j A . G j L + vol * . G j A . G j L = vol * . G j L + vol * i N + 1 . F i . G j
245 204 244 eqtrd φ j 1 M vol * . G j A = vol * . G j L + vol * i N + 1 . F i . G j
246 202 142 resubcld φ j 1 M vol * . G j A C M
247 inss2 . F i . G j . G j
248 190 adantr φ j 1 M i 1 N . G j
249 200 adantr φ j 1 M i 1 N vol * . G j
250 ovolsscl . F i . G j . G j . G j vol * . G j vol * . F i . G j
251 247 248 249 250 mp3an2i φ j 1 M i 1 N vol * . F i . G j
252 150 251 fsumrecl φ j 1 M i = 1 N vol * . F i . G j
253 15 r19.21bi φ j 1 M i = 1 N vol * . F i . G j vol * . G j A < C M
254 252 202 142 absdifltd φ j 1 M i = 1 N vol * . F i . G j vol * . G j A < C M vol * . G j A C M < i = 1 N vol * . F i . G j i = 1 N vol * . F i . G j < vol * . G j A + C M
255 253 254 mpbid φ j 1 M vol * . G j A C M < i = 1 N vol * . F i . G j i = 1 N vol * . F i . G j < vol * . G j A + C M
256 255 simpld φ j 1 M vol * . G j A C M < i = 1 N vol * . F i . G j
257 246 252 256 ltled φ j 1 M vol * . G j A C M i = 1 N vol * . F i . G j
258 149 fveq2d φ j 1 M vol * . G j L = vol * i = 1 N . F i . G j
259 mblvol . F i . G j dom vol vol . F i . G j = vol * . F i . G j
260 174 259 syl φ j 1 M i 1 N vol . F i . G j = vol * . F i . G j
261 260 251 eqeltrd φ j 1 M i 1 N vol . F i . G j
262 174 261 jca φ j 1 M i 1 N . F i . G j dom vol vol . F i . G j
263 262 ralrimiva φ j 1 M i 1 N . F i . G j dom vol vol . F i . G j
264 inss1 . F i . G j . F i
265 264 rgenw i . F i . G j . F i
266 222 adantr φ j 1 M Disj i . F i
267 disjss2 i . F i . G j . F i Disj i . F i Disj i . F i . G j
268 265 266 267 mpsyl φ j 1 M Disj i . F i . G j
269 disjss1 1 N Disj i . F i . G j Disj i = 1 N . F i . G j
270 223 268 269 mpsyl φ j 1 M Disj i = 1 N . F i . G j
271 volfiniun 1 N Fin i 1 N . F i . G j dom vol vol . F i . G j Disj i = 1 N . F i . G j vol i = 1 N . F i . G j = i = 1 N vol . F i . G j
272 150 263 270 271 syl3anc φ j 1 M vol i = 1 N . F i . G j = i = 1 N vol . F i . G j
273 mblvol i = 1 N . F i . G j dom vol vol i = 1 N . F i . G j = vol * i = 1 N . F i . G j
274 177 273 syl φ j 1 M vol i = 1 N . F i . G j = vol * i = 1 N . F i . G j
275 260 sumeq2dv φ j 1 M i = 1 N vol . F i . G j = i = 1 N vol * . F i . G j
276 272 274 275 3eqtr3d φ j 1 M vol * i = 1 N . F i . G j = i = 1 N vol * . F i . G j
277 258 276 eqtrd φ j 1 M vol * . G j L = i = 1 N vol * . F i . G j
278 257 277 breqtrrd φ j 1 M vol * . G j A C M vol * . G j L
279 277 252 eqeltrd φ j 1 M vol * . G j L
280 202 142 279 lesubaddd φ j 1 M vol * . G j A C M vol * . G j L vol * . G j A vol * . G j L + C M
281 278 280 mpbid φ j 1 M vol * . G j A vol * . G j L + C M
282 245 281 eqbrtrrd φ j 1 M vol * . G j L + vol * i N + 1 . F i . G j vol * . G j L + C M
283 134 142 279 leadd2d φ j 1 M vol * i N + 1 . F i . G j C M vol * . G j L + vol * i N + 1 . F i . G j vol * . G j L + C M
284 282 283 mpbird φ j 1 M vol * i N + 1 . F i . G j C M
285 127 134 142 284 fsumle φ j = 1 M vol * i N + 1 . F i . G j j = 1 M C M
286 141 recnd φ C M
287 fsumconst 1 M Fin C M j = 1 M C M = 1 M C M
288 127 286 287 syl2anc φ j = 1 M C M = 1 M C M
289 nnnn0 M M 0
290 hashfz1 M 0 1 M = M
291 11 289 290 3syl φ 1 M = M
292 291 oveq1d φ 1 M C M = M C M
293 119 recnd φ C
294 11 nncnd φ M
295 11 nnne0d φ M 0
296 293 294 295 divcan2d φ M C M = C
297 288 292 296 3eqtrd φ j = 1 M C M = C
298 285 297 breqtrd φ j = 1 M vol * i N + 1 . F i . G j C
299 117 135 119 140 298 letrd φ vol * j = 1 M i N + 1 . F i . G j C
300 117 119 39 299 leadd2dd φ vol * K L + vol * j = 1 M i N + 1 . F i . G j vol * K L + C
301 36 118 120 126 300 letrd φ vol * K A vol * K L + C