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 φDisjx.Fx
uniioombl.3 S=seq1+absF
uniioombl.a A=ran.F
uniioombl.e φvol*E
uniioombl.c φC+
uniioombl.g φG:2
uniioombl.s φEran.G
uniioombl.t T=seq1+absG
uniioombl.v φsupranT*<vol*E+C
uniioombl.m φM
uniioombl.m2 φTMsupranT*<<C
uniioombl.k K=.G1M
uniioombl.n φN
uniioombl.n2 φj1Mi=1Nvol*.Fi.Gjvol*.GjA<CM
uniioombl.l L=.F1N
Assertion uniioombllem4 φvol*KAvol*KL+C

Proof

Step Hyp Ref Expression
1 uniioombl.1 φF:2
2 uniioombl.2 φDisjx.Fx
3 uniioombl.3 S=seq1+absF
4 uniioombl.a A=ran.F
5 uniioombl.e φvol*E
6 uniioombl.c φC+
7 uniioombl.g φG:2
8 uniioombl.s φEran.G
9 uniioombl.t T=seq1+absG
10 uniioombl.v φsupranT*<vol*E+C
11 uniioombl.m φM
12 uniioombl.m2 φTMsupranT*<<C
13 uniioombl.k K=.G1M
14 uniioombl.n φN
15 uniioombl.n2 φj1Mi=1Nvol*.Fi.Gjvol*.GjA<CM
16 uniioombl.l L=.F1N
17 inss1 KAK
18 imassrn .G1Mran.G
19 18 unissi .G1Mran.G
20 13 19 eqsstri Kran.G
21 7 uniiccdif φran.Gran.Gvol*ran.Gran.G=0
22 21 simpld φran.Gran.G
23 ovolficcss G:2ran.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 φsupranT*<
28 ssid ran.Gran.G
29 9 ovollb G:2ran.Gran.Gvol*ran.GsupranT*<
30 7 28 29 sylancl φvol*ran.GsupranT*<
31 ovollecl ran.GsupranT*<vol*ran.GsupranT*<vol*ran.G
32 25 27 30 31 syl3anc φvol*ran.G
33 ovolsscl Kran.Gran.Gvol*ran.Gvol*K
34 20 25 32 33 mp3an2i φvol*K
35 ovolsscl KAKKvol*Kvol*KA
36 17 26 34 35 mp3an2i φvol*KA
37 inss1 KLK
38 ovolsscl KLKKvol*Kvol*KL
39 37 26 34 38 mp3an2i φvol*KL
40 ssun2 j=1MiN+1.Fi.GjKLj=1MiN+1.Fi.Gj
41 nnuz =1
42 14 peano2nnd φN+1
43 42 41 eleqtrdi φN+11
44 uzsplit N+111=1N+1-1N+1
45 43 44 syl φ1=1N+1-1N+1
46 41 45 eqtrid φ=1N+1-1N+1
47 14 nncnd φN
48 ax-1cn 1
49 pncan N1N+1-1=N
50 47 48 49 sylancl φN+1-1=N
51 50 oveq2d φ1N+1-1=1N
52 51 uneq1d φ1N+1-1N+1=1NN+1
53 46 52 eqtrd φ=1NN+1
54 53 iuneq1d φi.Fi=i1NN+1.Fi
55 iunxun i1NN+1.Fi=i=1N.FiiN+1.Fi
56 54 55 eqtrdi φi.Fi=i=1N.FiiN+1.Fi
57 ioof .:*×*𝒫
58 inss2 22
59 rexpssxrxp 2*×*
60 58 59 sstri 2*×*
61 fss F:22*×*F:*×*
62 1 60 61 sylancl φF:*×*
63 fco .:*×*𝒫F:*×*.F:𝒫
64 57 62 63 sylancr φ.F:𝒫
65 ffn .F:𝒫.FFn
66 fniunfv .FFni.Fi=ran.F
67 64 65 66 3syl φi.Fi=ran.F
68 fvco3 F:2i.Fi=.Fi
69 1 68 sylan φi.Fi=.Fi
70 69 iuneq2dv φi.Fi=i.Fi
71 67 70 eqtr3d φran.F=i.Fi
72 4 71 eqtrid φA=i.Fi
73 ffun .F:𝒫Fun.F
74 funiunfv Fun.Fi=1N.Fi=.F1N
75 64 73 74 3syl φi=1N.Fi=.F1N
76 elfznn i1Ni
77 1 76 68 syl2an φi1N.Fi=.Fi
78 77 iuneq2dv φi=1N.Fi=i=1N.Fi
79 75 78 eqtr3d φ.F1N=i=1N.Fi
80 16 79 eqtrid φL=i=1N.Fi
81 80 uneq1d φLiN+1.Fi=i=1N.FiiN+1.Fi
82 56 72 81 3eqtr4d φA=LiN+1.Fi
83 82 ineq2d φKA=KLiN+1.Fi
84 indi KLiN+1.Fi=KLKiN+1.Fi
85 83 84 eqtrdi φKA=KLKiN+1.Fi
86 fss G:22*×*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.Gj=1M.Gj=.G1M
92 89 90 91 3syl φj=1M.Gj=.G1M
93 elfznn j1Mj
94 fvco3 G:2j.Gj=.Gj
95 7 93 94 syl2an φj1M.Gj=.Gj
96 95 iuneq2dv φj=1M.Gj=j=1M.Gj
97 92 96 eqtr3d φ.G1M=j=1M.Gj
98 13 97 eqtrid φK=j=1M.Gj
99 98 ineq2d φiN+1.FiK=iN+1.Fij=1M.Gj
100 incom KiN+1.Fi=iN+1.FiK
101 iunin2 iN+1.Gj.Fi=.GjiN+1.Fi
102 incom .Fi.Gj=.Gj.Fi
103 102 a1i iN+1.Fi.Gj=.Gj.Fi
104 103 iuneq2i iN+1.Fi.Gj=iN+1.Gj.Fi
105 incom iN+1.Fi.Gj=.GjiN+1.Fi
106 101 104 105 3eqtr4ri iN+1.Fi.Gj=iN+1.Fi.Gj
107 106 a1i j1MiN+1.Fi.Gj=iN+1.Fi.Gj
108 107 iuneq2i j=1MiN+1.Fi.Gj=j=1MiN+1.Fi.Gj
109 iunin2 j=1MiN+1.Fi.Gj=iN+1.Fij=1M.Gj
110 108 109 eqtr3i j=1MiN+1.Fi.Gj=iN+1.Fij=1M.Gj
111 99 100 110 3eqtr4g φKiN+1.Fi=j=1MiN+1.Fi.Gj
112 111 uneq2d φKLKiN+1.Fi=KLj=1MiN+1.Fi.Gj
113 85 112 eqtrd φKA=KLj=1MiN+1.Fi.Gj
114 40 113 sseqtrrid φj=1MiN+1.Fi.GjKA
115 114 17 sstrdi φj=1MiN+1.Fi.GjK
116 ovolsscl j=1MiN+1.Fi.GjKKvol*Kvol*j=1MiN+1.Fi.Gj
117 115 26 34 116 syl3anc φvol*j=1MiN+1.Fi.Gj
118 39 117 readdcld φvol*KL+vol*j=1MiN+1.Fi.Gj
119 6 rpred φC
120 39 119 readdcld φvol*KL+C
121 113 fveq2d φvol*KA=vol*KLj=1MiN+1.Fi.Gj
122 37 26 sstrid φKL
123 115 26 sstrd φj=1MiN+1.Fi.Gj
124 ovolun KLvol*KLj=1MiN+1.Fi.Gjvol*j=1MiN+1.Fi.Gjvol*KLj=1MiN+1.Fi.Gjvol*KL+vol*j=1MiN+1.Fi.Gj
125 122 39 123 117 124 syl22anc φvol*KLj=1MiN+1.Fi.Gjvol*KL+vol*j=1MiN+1.Fi.Gj
126 121 125 eqbrtrd φvol*KAvol*KL+vol*j=1MiN+1.Fi.Gj
127 fzfid φ1MFin
128 iunss j=1MiN+1.Fi.GjKj1MiN+1.Fi.GjK
129 115 128 sylib φj1MiN+1.Fi.GjK
130 129 r19.21bi φj1MiN+1.Fi.GjK
131 26 adantr φj1MK
132 34 adantr φj1Mvol*K
133 ovolsscl iN+1.Fi.GjKKvol*Kvol*iN+1.Fi.Gj
134 130 131 132 133 syl3anc φj1Mvol*iN+1.Fi.Gj
135 127 134 fsumrecl φj=1Mvol*iN+1.Fi.Gj
136 130 131 sstrd φj1MiN+1.Fi.Gj
137 136 134 jca φj1MiN+1.Fi.Gjvol*iN+1.Fi.Gj
138 137 ralrimiva φj1MiN+1.Fi.Gjvol*iN+1.Fi.Gj
139 ovolfiniun 1MFinj1MiN+1.Fi.Gjvol*iN+1.Fi.Gjvol*j=1MiN+1.Fi.Gjj=1Mvol*iN+1.Fi.Gj
140 127 138 139 syl2anc φvol*j=1MiN+1.Fi.Gjj=1Mvol*iN+1.Fi.Gj
141 119 11 nndivred φCM
142 141 adantr φj1MCM
143 80 ineq2d φ.GjL=.Gji=1N.Fi
144 143 adantr φj1M.GjL=.Gji=1N.Fi
145 102 a1i i1N.Fi.Gj=.Gj.Fi
146 145 iuneq2i i=1N.Fi.Gj=i=1N.Gj.Fi
147 iunin2 i=1N.Gj.Fi=.Gji=1N.Fi
148 146 147 eqtri i=1N.Fi.Gj=.Gji=1N.Fi
149 144 148 eqtr4di φj1M.GjL=i=1N.Fi.Gj
150 fzfid φj1M1NFin
151 ffvelcdm F:2iFi2
152 1 76 151 syl2an φi1NFi2
153 152 elin2d φi1NFi2
154 1st2nd2 Fi2Fi=1stFi2ndFi
155 153 154 syl φi1NFi=1stFi2ndFi
156 155 fveq2d φi1N.Fi=.1stFi2ndFi
157 df-ov 1stFi2ndFi=.1stFi2ndFi
158 156 157 eqtr4di φi1N.Fi=1stFi2ndFi
159 ioombl 1stFi2ndFidomvol
160 158 159 eqeltrdi φi1N.Fidomvol
161 160 adantlr φj1Mi1N.Fidomvol
162 ffvelcdm G:2jGj2
163 7 93 162 syl2an φj1MGj2
164 163 elin2d φj1MGj2
165 1st2nd2 Gj2Gj=1stGj2ndGj
166 164 165 syl φj1MGj=1stGj2ndGj
167 166 fveq2d φj1M.Gj=.1stGj2ndGj
168 df-ov 1stGj2ndGj=.1stGj2ndGj
169 167 168 eqtr4di φj1M.Gj=1stGj2ndGj
170 ioombl 1stGj2ndGjdomvol
171 169 170 eqeltrdi φj1M.Gjdomvol
172 171 adantr φj1Mi1N.Gjdomvol
173 inmbl .Fidomvol.Gjdomvol.Fi.Gjdomvol
174 161 172 173 syl2anc φj1Mi1N.Fi.Gjdomvol
175 174 ralrimiva φj1Mi1N.Fi.Gjdomvol
176 finiunmbl 1NFini1N.Fi.Gjdomvoli=1N.Fi.Gjdomvol
177 150 175 176 syl2anc φj1Mi=1N.Fi.Gjdomvol
178 149 177 eqeltrd φj1M.GjLdomvol
179 inss2 .GjAA
180 1 uniiccdif φran.Fran.Fvol*ran.Fran.F=0
181 180 simpld φran.Fran.F
182 ovolficcss F:2ran.F
183 1 182 syl φran.F
184 181 183 sstrd φran.F
185 4 184 eqsstrid φA
186 185 adantr φj1MA
187 179 186 sstrid φj1M.GjA
188 inss1 .GjA.Gj
189 ioossre 1stGj2ndGj
190 169 189 eqsstrdi φj1M.Gj
191 169 fveq2d φj1Mvol*.Gj=vol*1stGj2ndGj
192 ovolfcl G:2j1stGj2ndGj1stGj2ndGj
193 7 93 192 syl2an φj1M1stGj2ndGj1stGj2ndGj
194 ovolioo 1stGj2ndGj1stGj2ndGjvol*1stGj2ndGj=2ndGj1stGj
195 193 194 syl φj1Mvol*1stGj2ndGj=2ndGj1stGj
196 191 195 eqtrd φj1Mvol*.Gj=2ndGj1stGj
197 193 simp2d φj1M2ndGj
198 193 simp1d φj1M1stGj
199 197 198 resubcld φj1M2ndGj1stGj
200 196 199 eqeltrd φj1Mvol*.Gj
201 ovolsscl .GjA.Gj.Gjvol*.Gjvol*.GjA
202 188 190 200 201 mp3an2i φj1Mvol*.GjA
203 mblsplit .GjLdomvol.GjAvol*.GjAvol*.GjA=vol*.GjA.GjL+vol*.GjA.GjL
204 178 187 202 203 syl3anc φj1Mvol*.GjA=vol*.GjA.GjL+vol*.GjA.GjL
205 imassrn .F1Nran.F
206 205 unissi .F1Nran.F
207 206 16 4 3sstr4i LA
208 sslin LA.GjL.GjA
209 207 208 mp1i φj1M.GjL.GjA
210 sseqin2 .GjL.GjA.GjA.GjL=.GjL
211 209 210 sylib φj1M.GjA.GjL=.GjL
212 211 fveq2d φj1Mvol*.GjA.GjL=vol*.GjL
213 indifdir AL.Gj=A.GjL.Gj
214 incom A.Gj=.GjA
215 incom L.Gj=.GjL
216 214 215 difeq12i A.GjL.Gj=.GjA.GjL
217 213 216 eqtri AL.Gj=.GjA.GjL
218 82 eqcomd φLiN+1.Fi=A
219 80 ineq1d φLiN+1.Fi=i=1N.FiiN+1.Fi
220 2fveq3 x=i.Fx=.Fi
221 220 cbvdisjv Disjx.FxDisji.Fi
222 2 221 sylib φDisji.Fi
223 fz1ssnn 1N
224 223 a1i φ1N
225 uzss N+11N+11
226 43 225 syl φN+11
227 226 41 sseqtrrdi φN+1
228 51 ineq1d φ1N+1-1N+1=1NN+1
229 uzdisj 1N+1-1N+1=
230 228 229 eqtr3di φ1NN+1=
231 disjiun Disji.Fi1NN+11NN+1=i=1N.FiiN+1.Fi=
232 222 224 227 230 231 syl13anc φi=1N.FiiN+1.Fi=
233 219 232 eqtrd φLiN+1.Fi=
234 uneqdifeq LALiN+1.Fi=LiN+1.Fi=AAL=iN+1.Fi
235 207 233 234 sylancr φLiN+1.Fi=AAL=iN+1.Fi
236 218 235 mpbid φAL=iN+1.Fi
237 236 adantr φj1MAL=iN+1.Fi
238 237 ineq2d φj1M.GjAL=.GjiN+1.Fi
239 incom AL.Gj=.GjAL
240 104 101 eqtri iN+1.Fi.Gj=.GjiN+1.Fi
241 238 239 240 3eqtr4g φj1MAL.Gj=iN+1.Fi.Gj
242 217 241 eqtr3id φj1M.GjA.GjL=iN+1.Fi.Gj
243 242 fveq2d φj1Mvol*.GjA.GjL=vol*iN+1.Fi.Gj
244 212 243 oveq12d φj1Mvol*.GjA.GjL+vol*.GjA.GjL=vol*.GjL+vol*iN+1.Fi.Gj
245 204 244 eqtrd φj1Mvol*.GjA=vol*.GjL+vol*iN+1.Fi.Gj
246 202 142 resubcld φj1Mvol*.GjACM
247 inss2 .Fi.Gj.Gj
248 190 adantr φj1Mi1N.Gj
249 200 adantr φj1Mi1Nvol*.Gj
250 ovolsscl .Fi.Gj.Gj.Gjvol*.Gjvol*.Fi.Gj
251 247 248 249 250 mp3an2i φj1Mi1Nvol*.Fi.Gj
252 150 251 fsumrecl φj1Mi=1Nvol*.Fi.Gj
253 15 r19.21bi φj1Mi=1Nvol*.Fi.Gjvol*.GjA<CM
254 252 202 142 absdifltd φj1Mi=1Nvol*.Fi.Gjvol*.GjA<CMvol*.GjACM<i=1Nvol*.Fi.Gji=1Nvol*.Fi.Gj<vol*.GjA+CM
255 253 254 mpbid φj1Mvol*.GjACM<i=1Nvol*.Fi.Gji=1Nvol*.Fi.Gj<vol*.GjA+CM
256 255 simpld φj1Mvol*.GjACM<i=1Nvol*.Fi.Gj
257 246 252 256 ltled φj1Mvol*.GjACMi=1Nvol*.Fi.Gj
258 149 fveq2d φj1Mvol*.GjL=vol*i=1N.Fi.Gj
259 mblvol .Fi.Gjdomvolvol.Fi.Gj=vol*.Fi.Gj
260 174 259 syl φj1Mi1Nvol.Fi.Gj=vol*.Fi.Gj
261 260 251 eqeltrd φj1Mi1Nvol.Fi.Gj
262 174 261 jca φj1Mi1N.Fi.Gjdomvolvol.Fi.Gj
263 262 ralrimiva φj1Mi1N.Fi.Gjdomvolvol.Fi.Gj
264 inss1 .Fi.Gj.Fi
265 264 rgenw i.Fi.Gj.Fi
266 222 adantr φj1MDisji.Fi
267 disjss2 i.Fi.Gj.FiDisji.FiDisji.Fi.Gj
268 265 266 267 mpsyl φj1MDisji.Fi.Gj
269 disjss1 1NDisji.Fi.GjDisji=1N.Fi.Gj
270 223 268 269 mpsyl φj1MDisji=1N.Fi.Gj
271 volfiniun 1NFini1N.Fi.Gjdomvolvol.Fi.GjDisji=1N.Fi.Gjvoli=1N.Fi.Gj=i=1Nvol.Fi.Gj
272 150 263 270 271 syl3anc φj1Mvoli=1N.Fi.Gj=i=1Nvol.Fi.Gj
273 mblvol i=1N.Fi.Gjdomvolvoli=1N.Fi.Gj=vol*i=1N.Fi.Gj
274 177 273 syl φj1Mvoli=1N.Fi.Gj=vol*i=1N.Fi.Gj
275 260 sumeq2dv φj1Mi=1Nvol.Fi.Gj=i=1Nvol*.Fi.Gj
276 272 274 275 3eqtr3d φj1Mvol*i=1N.Fi.Gj=i=1Nvol*.Fi.Gj
277 258 276 eqtrd φj1Mvol*.GjL=i=1Nvol*.Fi.Gj
278 257 277 breqtrrd φj1Mvol*.GjACMvol*.GjL
279 277 252 eqeltrd φj1Mvol*.GjL
280 202 142 279 lesubaddd φj1Mvol*.GjACMvol*.GjLvol*.GjAvol*.GjL+CM
281 278 280 mpbid φj1Mvol*.GjAvol*.GjL+CM
282 245 281 eqbrtrrd φj1Mvol*.GjL+vol*iN+1.Fi.Gjvol*.GjL+CM
283 134 142 279 leadd2d φj1Mvol*iN+1.Fi.GjCMvol*.GjL+vol*iN+1.Fi.Gjvol*.GjL+CM
284 282 283 mpbird φj1Mvol*iN+1.Fi.GjCM
285 127 134 142 284 fsumle φj=1Mvol*iN+1.Fi.Gjj=1MCM
286 141 recnd φCM
287 fsumconst 1MFinCMj=1MCM=1MCM
288 127 286 287 syl2anc φj=1MCM=1MCM
289 nnnn0 MM0
290 hashfz1 M01M=M
291 11 289 290 3syl φ1M=M
292 291 oveq1d φ1MCM=MCM
293 119 recnd φC
294 11 nncnd φM
295 11 nnne0d φM0
296 293 294 295 divcan2d φMCM=C
297 288 292 296 3eqtrd φj=1MCM=C
298 285 297 breqtrd φj=1Mvol*iN+1.Fi.GjC
299 117 135 119 140 298 letrd φvol*j=1MiN+1.Fi.GjC
300 117 119 39 299 leadd2dd φvol*KL+vol*j=1MiN+1.Fi.Gjvol*KL+C
301 36 118 120 126 300 letrd φvol*KAvol*KL+C