Metamath Proof Explorer


Theorem ismblfin

Description: Measurability in terms of inner and outer measure. Proposition 7 of Viaclovsky8 p. 3. (Contributed by Brendan Leahy, 4-Mar-2018) (Revised by Brendan Leahy, 28-Mar-2018)

Ref Expression
Assertion ismblfin A vol * A A dom vol vol * A = sup y | b Clsd topGen ran . b A y = vol b <

Proof

Step Hyp Ref Expression
1 mblfinlem4 A vol * A A dom vol vol * A = sup y | b Clsd topGen ran . b A y = vol b <
2 elpwi w 𝒫 w
3 elmapi f 2 f : 2
4 inss1 w A w
5 ovolsscl w A w w vol * w vol * w A
6 4 5 mp3an1 w vol * w vol * w A
7 difss w A w
8 ovolsscl w A w w vol * w vol * w A
9 7 8 mp3an1 w vol * w vol * w A
10 6 9 readdcld w vol * w vol * w A + vol * w A
11 10 rexrd w vol * w vol * w A + vol * w A *
12 11 ad3antlr A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w f : 2 w ran . f vol * w A + vol * w A *
13 rncoss ran . f ran .
14 13 unissi ran . f ran .
15 unirnioo = ran .
16 14 15 sseqtrri ran . f
17 ovolcl ran . f vol * ran . f *
18 16 17 mp1i A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w f : 2 w ran . f vol * ran . f *
19 eqid abs f = abs f
20 eqid seq 1 + abs f = seq 1 + abs f
21 19 20 ovolsf f : 2 seq 1 + abs f : 0 +∞
22 frn seq 1 + abs f : 0 +∞ ran seq 1 + abs f 0 +∞
23 icossxr 0 +∞ *
24 22 23 sstrdi seq 1 + abs f : 0 +∞ ran seq 1 + abs f *
25 supxrcl ran seq 1 + abs f * sup ran seq 1 + abs f * < *
26 21 24 25 3syl f : 2 sup ran seq 1 + abs f * < *
27 26 ad2antlr A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w f : 2 w ran . f sup ran seq 1 + abs f * < *
28 pnfge vol * w A + vol * w A * vol * w A + vol * w A +∞
29 11 28 syl w vol * w vol * w A + vol * w A +∞
30 29 ad2antrr w vol * w w ran . f vol * ran . f = +∞ vol * w A + vol * w A +∞
31 simpr w vol * w w ran . f vol * ran . f = +∞ vol * ran . f = +∞
32 30 31 breqtrrd w vol * w w ran . f vol * ran . f = +∞ vol * w A + vol * w A vol * ran . f
33 32 adantlll A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f vol * ran . f = +∞ vol * w A + vol * w A vol * ran . f
34 16 17 ax-mp vol * ran . f *
35 nltpnft vol * ran . f * vol * ran . f = +∞ ¬ vol * ran . f < +∞
36 34 35 ax-mp vol * ran . f = +∞ ¬ vol * ran . f < +∞
37 36 necon2abii vol * ran . f < +∞ vol * ran . f +∞
38 ovolge0 ran . f 0 vol * ran . f
39 16 38 ax-mp 0 vol * ran . f
40 0re 0
41 xrre3 vol * ran . f * 0 0 vol * ran . f vol * ran . f < +∞ vol * ran . f
42 34 40 41 mpanl12 0 vol * ran . f vol * ran . f < +∞ vol * ran . f
43 39 42 mpan vol * ran . f < +∞ vol * ran . f
44 37 43 sylbir vol * ran . f +∞ vol * ran . f
45 10 ad3antlr A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f vol * ran . f vol * w A + vol * w A
46 simpr a ran . f A z = vol a z = vol a
47 eleq1w b = a b dom vol a dom vol
48 uniretop = topGen ran .
49 48 cldss b Clsd topGen ran . b
50 dfss4 b b = b
51 49 50 sylib b Clsd topGen ran . b = b
52 rembl dom vol
53 48 cldopn b Clsd topGen ran . b topGen ran .
54 opnmbl b topGen ran . b dom vol
55 53 54 syl b Clsd topGen ran . b dom vol
56 difmbl dom vol b dom vol b dom vol
57 52 55 56 sylancr b Clsd topGen ran . b dom vol
58 51 57 eqeltrrd b Clsd topGen ran . b dom vol
59 47 58 vtoclga a Clsd topGen ran . a dom vol
60 mblvol a dom vol vol a = vol * a
61 59 60 syl a Clsd topGen ran . vol a = vol * a
62 46 61 sylan9eqr a Clsd topGen ran . a ran . f A z = vol a z = vol * a
63 62 adantl vol * ran . f a Clsd topGen ran . a ran . f A z = vol a z = vol * a
64 inss1 ran . f A ran . f
65 sstr a ran . f A ran . f A ran . f a ran . f
66 64 65 mpan2 a ran . f A a ran . f
67 66 ad2antrl a Clsd topGen ran . a ran . f A z = vol a a ran . f
68 ovolsscl a ran . f ran . f vol * ran . f vol * a
69 16 68 mp3an2 a ran . f vol * ran . f vol * a
70 69 ancoms vol * ran . f a ran . f vol * a
71 67 70 sylan2 vol * ran . f a Clsd topGen ran . a ran . f A z = vol a vol * a
72 63 71 eqeltrd vol * ran . f a Clsd topGen ran . a ran . f A z = vol a z
73 72 rexlimdvaa vol * ran . f a Clsd topGen ran . a ran . f A z = vol a z
74 73 abssdv vol * ran . f z | a Clsd topGen ran . a ran . f A z = vol a
75 eqeq1 z = y z = vol a y = vol a
76 75 anbi2d z = y a ran . f A z = vol a a ran . f A y = vol a
77 76 rexbidv z = y a Clsd topGen ran . a ran . f A z = vol a a Clsd topGen ran . a ran . f A y = vol a
78 77 ralab y z | a Clsd topGen ran . a ran . f A z = vol a y vol * ran . f y a Clsd topGen ran . a ran . f A y = vol a y vol * ran . f
79 simpr a ran . f A y = vol a y = vol a
80 79 61 sylan9eqr a Clsd topGen ran . a ran . f A y = vol a y = vol * a
81 ovolss a ran . f ran . f vol * a vol * ran . f
82 66 16 81 sylancl a ran . f A vol * a vol * ran . f
83 82 ad2antrl a Clsd topGen ran . a ran . f A y = vol a vol * a vol * ran . f
84 80 83 eqbrtrd a Clsd topGen ran . a ran . f A y = vol a y vol * ran . f
85 84 rexlimiva a Clsd topGen ran . a ran . f A y = vol a y vol * ran . f
86 78 85 mpgbir y z | a Clsd topGen ran . a ran . f A z = vol a y vol * ran . f
87 brralrspcev vol * ran . f y z | a Clsd topGen ran . a ran . f A z = vol a y vol * ran . f x y z | a Clsd topGen ran . a ran . f A z = vol a y x
88 86 87 mpan2 vol * ran . f x y z | a Clsd topGen ran . a ran . f A z = vol a y x
89 retop topGen ran . Top
90 0cld topGen ran . Top Clsd topGen ran .
91 89 90 ax-mp Clsd topGen ran .
92 0ss ran . f A
93 0mbl dom vol
94 mblvol dom vol vol = vol *
95 93 94 ax-mp vol = vol *
96 ovol0 vol * = 0
97 95 96 eqtr2i 0 = vol
98 92 97 pm3.2i ran . f A 0 = vol
99 sseq1 a = a ran . f A ran . f A
100 fveq2 a = vol a = vol
101 100 eqeq2d a = 0 = vol a 0 = vol
102 99 101 anbi12d a = a ran . f A 0 = vol a ran . f A 0 = vol
103 102 rspcev Clsd topGen ran . ran . f A 0 = vol a Clsd topGen ran . a ran . f A 0 = vol a
104 91 98 103 mp2an a Clsd topGen ran . a ran . f A 0 = vol a
105 c0ex 0 V
106 eqeq1 z = 0 z = vol a 0 = vol a
107 106 anbi2d z = 0 a ran . f A z = vol a a ran . f A 0 = vol a
108 107 rexbidv z = 0 a Clsd topGen ran . a ran . f A z = vol a a Clsd topGen ran . a ran . f A 0 = vol a
109 105 108 elab 0 z | a Clsd topGen ran . a ran . f A z = vol a a Clsd topGen ran . a ran . f A 0 = vol a
110 104 109 mpbir 0 z | a Clsd topGen ran . a ran . f A z = vol a
111 110 ne0ii z | a Clsd topGen ran . a ran . f A z = vol a
112 suprcl z | a Clsd topGen ran . a ran . f A z = vol a z | a Clsd topGen ran . a ran . f A z = vol a x y z | a Clsd topGen ran . a ran . f A z = vol a y x sup z | a Clsd topGen ran . a ran . f A z = vol a <
113 111 112 mp3an2 z | a Clsd topGen ran . a ran . f A z = vol a x y z | a Clsd topGen ran . a ran . f A z = vol a y x sup z | a Clsd topGen ran . a ran . f A z = vol a <
114 74 88 113 syl2anc vol * ran . f sup z | a Clsd topGen ran . a ran . f A z = vol a <
115 simpr c ran . f A z = vol c z = vol c
116 eleq1w b = c b dom vol c dom vol
117 116 58 vtoclga c Clsd topGen ran . c dom vol
118 mblvol c dom vol vol c = vol * c
119 117 118 syl c Clsd topGen ran . vol c = vol * c
120 115 119 sylan9eqr c Clsd topGen ran . c ran . f A z = vol c z = vol * c
121 120 adantl vol * ran . f c Clsd topGen ran . c ran . f A z = vol c z = vol * c
122 difss2 c ran . f A c ran . f
123 122 ad2antrl c Clsd topGen ran . c ran . f A z = vol c c ran . f
124 ovolsscl c ran . f ran . f vol * ran . f vol * c
125 16 124 mp3an2 c ran . f vol * ran . f vol * c
126 125 ancoms vol * ran . f c ran . f vol * c
127 123 126 sylan2 vol * ran . f c Clsd topGen ran . c ran . f A z = vol c vol * c
128 121 127 eqeltrd vol * ran . f c Clsd topGen ran . c ran . f A z = vol c z
129 128 rexlimdvaa vol * ran . f c Clsd topGen ran . c ran . f A z = vol c z
130 129 abssdv vol * ran . f z | c Clsd topGen ran . c ran . f A z = vol c
131 eqeq1 z = y z = vol c y = vol c
132 131 anbi2d z = y c ran . f A z = vol c c ran . f A y = vol c
133 132 rexbidv z = y c Clsd topGen ran . c ran . f A z = vol c c Clsd topGen ran . c ran . f A y = vol c
134 133 ralab y z | c Clsd topGen ran . c ran . f A z = vol c y vol * ran . f y c Clsd topGen ran . c ran . f A y = vol c y vol * ran . f
135 simpr c ran . f A y = vol c y = vol c
136 135 119 sylan9eqr c Clsd topGen ran . c ran . f A y = vol c y = vol * c
137 ovolss c ran . f ran . f vol * c vol * ran . f
138 122 16 137 sylancl c ran . f A vol * c vol * ran . f
139 138 ad2antrl c Clsd topGen ran . c ran . f A y = vol c vol * c vol * ran . f
140 136 139 eqbrtrd c Clsd topGen ran . c ran . f A y = vol c y vol * ran . f
141 140 rexlimiva c Clsd topGen ran . c ran . f A y = vol c y vol * ran . f
142 134 141 mpgbir y z | c Clsd topGen ran . c ran . f A z = vol c y vol * ran . f
143 brralrspcev vol * ran . f y z | c Clsd topGen ran . c ran . f A z = vol c y vol * ran . f x y z | c Clsd topGen ran . c ran . f A z = vol c y x
144 142 143 mpan2 vol * ran . f x y z | c Clsd topGen ran . c ran . f A z = vol c y x
145 0ss ran . f A
146 145 97 pm3.2i ran . f A 0 = vol
147 sseq1 c = c ran . f A ran . f A
148 fveq2 c = vol c = vol
149 148 eqeq2d c = 0 = vol c 0 = vol
150 147 149 anbi12d c = c ran . f A 0 = vol c ran . f A 0 = vol
151 150 rspcev Clsd topGen ran . ran . f A 0 = vol c Clsd topGen ran . c ran . f A 0 = vol c
152 91 146 151 mp2an c Clsd topGen ran . c ran . f A 0 = vol c
153 eqeq1 z = 0 z = vol c 0 = vol c
154 153 anbi2d z = 0 c ran . f A z = vol c c ran . f A 0 = vol c
155 154 rexbidv z = 0 c Clsd topGen ran . c ran . f A z = vol c c Clsd topGen ran . c ran . f A 0 = vol c
156 105 155 elab 0 z | c Clsd topGen ran . c ran . f A z = vol c c Clsd topGen ran . c ran . f A 0 = vol c
157 152 156 mpbir 0 z | c Clsd topGen ran . c ran . f A z = vol c
158 157 ne0ii z | c Clsd topGen ran . c ran . f A z = vol c
159 suprcl z | c Clsd topGen ran . c ran . f A z = vol c z | c Clsd topGen ran . c ran . f A z = vol c x y z | c Clsd topGen ran . c ran . f A z = vol c y x sup z | c Clsd topGen ran . c ran . f A z = vol c <
160 158 159 mp3an2 z | c Clsd topGen ran . c ran . f A z = vol c x y z | c Clsd topGen ran . c ran . f A z = vol c y x sup z | c Clsd topGen ran . c ran . f A z = vol c <
161 130 144 160 syl2anc vol * ran . f sup z | c Clsd topGen ran . c ran . f A z = vol c <
162 114 161 readdcld vol * ran . f sup z | a Clsd topGen ran . a ran . f A z = vol a < + sup z | c Clsd topGen ran . c ran . f A z = vol c <
163 162 adantl A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f vol * ran . f sup z | a Clsd topGen ran . a ran . f A z = vol a < + sup z | c Clsd topGen ran . c ran . f A z = vol c <
164 simpr A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f vol * ran . f vol * ran . f
165 6 ad2antrr w vol * w w ran . f vol * ran . f vol * w A
166 9 ad2antrr w vol * w w ran . f vol * ran . f vol * w A
167 ovolsscl ran . f A ran . f ran . f vol * ran . f vol * ran . f A
168 64 16 167 mp3an12 vol * ran . f vol * ran . f A
169 168 adantl w vol * w w ran . f vol * ran . f vol * ran . f A
170 difss ran . f A ran . f
171 ovolsscl ran . f A ran . f ran . f vol * ran . f vol * ran . f A
172 170 16 171 mp3an12 vol * ran . f vol * ran . f A
173 172 adantl w vol * w w ran . f vol * ran . f vol * ran . f A
174 ssrin w ran . f w A ran . f A
175 64 16 sstri ran . f A
176 ovolss w A ran . f A ran . f A vol * w A vol * ran . f A
177 174 175 176 sylancl w ran . f vol * w A vol * ran . f A
178 177 ad2antlr w vol * w w ran . f vol * ran . f vol * w A vol * ran . f A
179 ssdif w ran . f w A ran . f A
180 170 16 sstri ran . f A
181 ovolss w A ran . f A ran . f A vol * w A vol * ran . f A
182 179 180 181 sylancl w ran . f vol * w A vol * ran . f A
183 182 ad2antlr w vol * w w ran . f vol * ran . f vol * w A vol * ran . f A
184 165 166 169 173 178 183 le2addd w vol * w w ran . f vol * ran . f vol * w A + vol * w A vol * ran . f A + vol * ran . f A
185 dfin4 ran . f A = ran . f ran . f A
186 185 fveq2i vol * ran . f A = vol * ran . f ran . f A
187 186 oveq1i vol * ran . f A + vol * ran . f A = vol * ran . f ran . f A + vol * ran . f A
188 184 187 breqtrdi w vol * w w ran . f vol * ran . f vol * w A + vol * w A vol * ran . f ran . f A + vol * ran . f A
189 188 adantlll A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f vol * ran . f vol * w A + vol * w A vol * ran . f ran . f A + vol * ran . f A
190 simpll A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b <
191 185 sseq2i a ran . f A a ran . f ran . f A
192 191 anbi1i a ran . f A z = vol a a ran . f ran . f A z = vol a
193 192 rexbii a Clsd topGen ran . a ran . f A z = vol a a Clsd topGen ran . a ran . f ran . f A z = vol a
194 193 abbii z | a Clsd topGen ran . a ran . f A z = vol a = z | a Clsd topGen ran . a ran . f ran . f A z = vol a
195 194 supeq1i sup z | a Clsd topGen ran . a ran . f A z = vol a < = sup z | a Clsd topGen ran . a ran . f ran . f A z = vol a <
196 16 jctl vol * ran . f ran . f vol * ran . f
197 196 adantl A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f ran . f vol * ran . f
198 172 180 jctil vol * ran . f ran . f A vol * ran . f A
199 198 adantl A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f ran . f A vol * ran . f A
200 ltso < Or
201 200 a1i vol * ran . f < Or
202 id vol * ran . f vol * ran . f
203 vex x V
204 eqeq1 z = x z = vol c x = vol c
205 204 anbi2d z = x c ran . f z = vol c c ran . f x = vol c
206 205 rexbidv z = x c Clsd topGen ran . c ran . f z = vol c c Clsd topGen ran . c ran . f x = vol c
207 203 206 elab x z | c Clsd topGen ran . c ran . f z = vol c c Clsd topGen ran . c ran . f x = vol c
208 16 137 mpan2 c ran . f vol * c vol * ran . f
209 208 ad2antrl c Clsd topGen ran . c ran . f x = vol c vol * c vol * ran . f
210 48 cldss c Clsd topGen ran . c
211 ovolcl c vol * c *
212 210 211 syl c Clsd topGen ran . vol * c *
213 xrlenlt vol * c * vol * ran . f * vol * c vol * ran . f ¬ vol * ran . f < vol * c
214 212 34 213 sylancl c Clsd topGen ran . vol * c vol * ran . f ¬ vol * ran . f < vol * c
215 214 adantr c Clsd topGen ran . c ran . f x = vol c vol * c vol * ran . f ¬ vol * ran . f < vol * c
216 id x = vol c x = vol c
217 216 119 sylan9eqr c Clsd topGen ran . x = vol c x = vol * c
218 breq2 x = vol * c vol * ran . f < x vol * ran . f < vol * c
219 218 notbid x = vol * c ¬ vol * ran . f < x ¬ vol * ran . f < vol * c
220 217 219 syl c Clsd topGen ran . x = vol c ¬ vol * ran . f < x ¬ vol * ran . f < vol * c
221 220 adantrl c Clsd topGen ran . c ran . f x = vol c ¬ vol * ran . f < x ¬ vol * ran . f < vol * c
222 215 221 bitr4d c Clsd topGen ran . c ran . f x = vol c vol * c vol * ran . f ¬ vol * ran . f < x
223 209 222 mpbid c Clsd topGen ran . c ran . f x = vol c ¬ vol * ran . f < x
224 223 rexlimiva c Clsd topGen ran . c ran . f x = vol c ¬ vol * ran . f < x
225 207 224 sylbi x z | c Clsd topGen ran . c ran . f z = vol c ¬ vol * ran . f < x
226 225 adantl vol * ran . f x z | c Clsd topGen ran . c ran . f z = vol c ¬ vol * ran . f < x
227 retopbas ran . TopBases
228 bastg ran . TopBases ran . topGen ran .
229 227 228 ax-mp ran . topGen ran .
230 13 229 sstri ran . f topGen ran .
231 uniopn topGen ran . Top ran . f topGen ran . ran . f topGen ran .
232 89 230 231 mp2an ran . f topGen ran .
233 mblfinlem2 ran . f topGen ran . x x < vol * ran . f c Clsd topGen ran . c ran . f x < vol * c
234 232 233 mp3an1 x x < vol * ran . f c Clsd topGen ran . c ran . f x < vol * c
235 119 eqcomd c Clsd topGen ran . vol * c = vol c
236 235 anim1i c Clsd topGen ran . x < vol * c vol * c = vol c x < vol * c
237 236 ex c Clsd topGen ran . x < vol * c vol * c = vol c x < vol * c
238 237 anim2d c Clsd topGen ran . c ran . f x < vol * c c ran . f vol * c = vol c x < vol * c
239 fvex vol * c V
240 eqeq1 y = vol * c y = vol c vol * c = vol c
241 240 anbi2d y = vol * c c ran . f y = vol c c ran . f vol * c = vol c
242 breq2 y = vol * c x < y x < vol * c
243 241 242 anbi12d y = vol * c c ran . f y = vol c x < y c ran . f vol * c = vol c x < vol * c
244 239 243 spcev c ran . f vol * c = vol c x < vol * c y c ran . f y = vol c x < y
245 244 anasss c ran . f vol * c = vol c x < vol * c y c ran . f y = vol c x < y
246 238 245 syl6 c Clsd topGen ran . c ran . f x < vol * c y c ran . f y = vol c x < y
247 246 reximia c Clsd topGen ran . c ran . f x < vol * c c Clsd topGen ran . y c ran . f y = vol c x < y
248 234 247 syl x x < vol * ran . f c Clsd topGen ran . y c ran . f y = vol c x < y
249 r19.41v c Clsd topGen ran . c ran . f y = vol c x < y c Clsd topGen ran . c ran . f y = vol c x < y
250 249 exbii y c Clsd topGen ran . c ran . f y = vol c x < y y c Clsd topGen ran . c ran . f y = vol c x < y
251 rexcom4 c Clsd topGen ran . y c ran . f y = vol c x < y y c Clsd topGen ran . c ran . f y = vol c x < y
252 131 anbi2d z = y c ran . f z = vol c c ran . f y = vol c
253 252 rexbidv z = y c Clsd topGen ran . c ran . f z = vol c c Clsd topGen ran . c ran . f y = vol c
254 253 rexab y z | c Clsd topGen ran . c ran . f z = vol c x < y y c Clsd topGen ran . c ran . f y = vol c x < y
255 250 251 254 3bitr4i c Clsd topGen ran . y c ran . f y = vol c x < y y z | c Clsd topGen ran . c ran . f z = vol c x < y
256 248 255 sylib x x < vol * ran . f y z | c Clsd topGen ran . c ran . f z = vol c x < y
257 256 adantl vol * ran . f x x < vol * ran . f y z | c Clsd topGen ran . c ran . f z = vol c x < y
258 201 202 226 257 eqsupd vol * ran . f sup z | c Clsd topGen ran . c ran . f z = vol c < = vol * ran . f
259 258 eqcomd vol * ran . f vol * ran . f = sup z | c Clsd topGen ran . c ran . f z = vol c <
260 259 adantl A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f vol * ran . f = sup z | c Clsd topGen ran . c ran . f z = vol c <
261 sseq1 c = a c ran . f a ran . f
262 fveq2 c = a vol c = vol a
263 262 eqeq2d c = a z = vol c z = vol a
264 261 263 anbi12d c = a c ran . f z = vol c a ran . f z = vol a
265 264 cbvrexvw c Clsd topGen ran . c ran . f z = vol c a Clsd topGen ran . a ran . f z = vol a
266 265 abbii z | c Clsd topGen ran . c ran . f z = vol c = z | a Clsd topGen ran . a ran . f z = vol a
267 266 supeq1i sup z | c Clsd topGen ran . c ran . f z = vol c < = sup z | a Clsd topGen ran . a ran . f z = vol a <
268 260 267 syl6eq A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f vol * ran . f = sup z | a Clsd topGen ran . a ran . f z = vol a <
269 sseq1 c = a c ran . f A a ran . f A
270 269 263 anbi12d c = a c ran . f A z = vol c a ran . f A z = vol a
271 270 cbvrexvw c Clsd topGen ran . c ran . f A z = vol c a Clsd topGen ran . a ran . f A z = vol a
272 271 abbii z | c Clsd topGen ran . c ran . f A z = vol c = z | a Clsd topGen ran . a ran . f A z = vol a
273 272 supeq1i sup z | c Clsd topGen ran . c ran . f A z = vol c < = sup z | a Clsd topGen ran . a ran . f A z = vol a <
274 simpll A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f A vol * A
275 eqeq1 y = z y = vol b z = vol b
276 275 anbi2d y = z b A y = vol b b A z = vol b
277 276 rexbidv y = z b Clsd topGen ran . b A y = vol b b Clsd topGen ran . b A z = vol b
278 sseq1 b = c b A c A
279 fveq2 b = c vol b = vol c
280 279 eqeq2d b = c z = vol b z = vol c
281 278 280 anbi12d b = c b A z = vol b c A z = vol c
282 281 cbvrexvw b Clsd topGen ran . b A z = vol b c Clsd topGen ran . c A z = vol c
283 277 282 syl6bb y = z b Clsd topGen ran . b A y = vol b c Clsd topGen ran . c A z = vol c
284 283 cbvabv y | b Clsd topGen ran . b A y = vol b = z | c Clsd topGen ran . c A z = vol c
285 284 supeq1i sup y | b Clsd topGen ran . b A y = vol b < = sup z | c Clsd topGen ran . c A z = vol c <
286 285 eqeq2i vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * A = sup z | c Clsd topGen ran . c A z = vol c <
287 286 biimpi vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * A = sup z | c Clsd topGen ran . c A z = vol c <
288 287 ad2antlr A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f vol * A = sup z | c Clsd topGen ran . c A z = vol c <
289 mblfinlem3 ran . f vol * ran . f A vol * A vol * ran . f = sup z | c Clsd topGen ran . c ran . f z = vol c < vol * A = sup z | c Clsd topGen ran . c A z = vol c < sup z | c Clsd topGen ran . c ran . f A z = vol c < = vol * ran . f A
290 197 274 260 288 289 syl112anc A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f sup z | c Clsd topGen ran . c ran . f A z = vol c < = vol * ran . f A
291 273 290 syl5reqr A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f vol * ran . f A = sup z | a Clsd topGen ran . a ran . f A z = vol a <
292 mblfinlem3 ran . f vol * ran . f ran . f A vol * ran . f A vol * ran . f = sup z | a Clsd topGen ran . a ran . f z = vol a < vol * ran . f A = sup z | a Clsd topGen ran . a ran . f A z = vol a < sup z | a Clsd topGen ran . a ran . f ran . f A z = vol a < = vol * ran . f ran . f A
293 197 199 268 291 292 syl112anc A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f sup z | a Clsd topGen ran . a ran . f ran . f A z = vol a < = vol * ran . f ran . f A
294 195 293 syl5eq A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f sup z | a Clsd topGen ran . a ran . f A z = vol a < = vol * ran . f ran . f A
295 294 290 oveq12d A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < vol * ran . f sup z | a Clsd topGen ran . a ran . f A z = vol a < + sup z | c Clsd topGen ran . c ran . f A z = vol c < = vol * ran . f ran . f A + vol * ran . f A
296 190 295 sylan A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f vol * ran . f sup z | a Clsd topGen ran . a ran . f A z = vol a < + sup z | c Clsd topGen ran . c ran . f A z = vol c < = vol * ran . f ran . f A + vol * ran . f A
297 189 296 breqtrrd A vol * A vol * A = sup y | b Clsd topGen ran . b A y = vol b < w vol * w w ran . f vol * ran . f vol * w A + vol * w A sup z | a Clsd topGen ran . a ran . f A z = vol a < + sup z | c Clsd topGen ran . c ran . f A z = vol c <
298 ne0i 0 z | a Clsd topGen ran . a ran . f A z = vol a z | a Clsd topGen ran . a ran . f A z = vol a
299 110 298 mp1i vol * ran . f z | a Clsd topGen ran . a ran . f A z = vol a
300 ne0i 0 z | c Clsd topGen ran . c ran . f A z = vol c z | c Clsd topGen ran . c ran . f A z = vol c
301 157 300 mp1i vol * ran . f z | c Clsd topGen ran . c ran . f A z = vol c
302 eqid t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v = t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v
303 74 299 88 130 301 144 302 supadd vol * ran . f sup z | a Clsd topGen ran . a ran . f A z = vol a < + sup z | c Clsd topGen ran . c ran . f A z = vol c < = sup t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v <
304 reeanv a Clsd topGen ran . c Clsd topGen ran . a ran . f A u = vol a c ran . f A v = vol c a Clsd topGen ran . a ran . f A u = vol a c Clsd topGen ran . c ran . f A v = vol c
305 vex u V
306 eqeq1 z = u z = vol a u = vol a
307 306 anbi2d z = u a ran . f A z = vol a a ran . f A u = vol a
308 307 rexbidv z = u a Clsd topGen ran . a ran . f A z = vol a a Clsd topGen ran . a ran . f A u = vol a
309 305 308 elab u z | a Clsd topGen ran . a ran . f A z = vol a a Clsd topGen ran . a ran . f A u = vol a
310 vex v V
311 eqeq1 z = v z = vol c v = vol c
312 311 anbi2d z = v c ran . f A z = vol c c ran . f A v = vol c
313 312 rexbidv z = v c Clsd topGen ran . c ran . f A z = vol c c Clsd topGen ran . c ran . f A v = vol c
314 310 313 elab v z | c Clsd topGen ran . c ran . f A z = vol c c Clsd topGen ran . c ran . f A v = vol c
315 309 314 anbi12i u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c a Clsd topGen ran . a ran . f A u = vol a c Clsd topGen ran . c ran . f A v = vol c
316 304 315 bitr4i a Clsd topGen ran . c Clsd topGen ran . a ran . f A u = vol a c ran . f A v = vol c u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c
317 an4 a ran . f A c ran . f A u = vol a v = vol c a ran . f A u = vol a c ran . f A v = vol c
318 oveq12 u = vol a v = vol c u + v = vol a + vol c
319 59 adantr a Clsd topGen ran . c Clsd topGen ran . a dom vol
320 319 ad2antlr vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A a dom vol
321 117 adantl a Clsd topGen ran . c Clsd topGen ran . c dom vol
322 321 ad2antlr vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A c dom vol
323 ss2in a ran . f A c ran . f A a c ran . f A ran . f A
324 185 ineq1i ran . f A ran . f A = ran . f ran . f A ran . f A
325 incom ran . f ran . f A ran . f A = ran . f A ran . f ran . f A
326 disjdif ran . f A ran . f ran . f A =
327 324 325 326 3eqtri ran . f A ran . f A =
328 323 327 sseqtrdi a ran . f A c ran . f A a c
329 ss0 a c a c =
330 328 329 syl a ran . f A c ran . f A a c =
331 330 adantl vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A a c =
332 61 adantr a Clsd topGen ran . c Clsd topGen ran . vol a = vol * a
333 332 ad2antlr vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol a = vol * a
334 66 16 jctir a ran . f A a ran . f ran . f
335 68 3expa a ran . f ran . f vol * ran . f vol * a
336 334 335 sylan a ran . f A vol * ran . f vol * a
337 336 ancoms vol * ran . f a ran . f A vol * a
338 337 ad2ant2r vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol * a
339 333 338 eqeltrd vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol a
340 119 adantl a Clsd topGen ran . c Clsd topGen ran . vol c = vol * c
341 340 ad2antlr vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol c = vol * c
342 122 16 jctir c ran . f A c ran . f ran . f
343 124 3expa c ran . f ran . f vol * ran . f vol * c
344 342 343 sylan c ran . f A vol * ran . f vol * c
345 344 ancoms vol * ran . f c ran . f A vol * c
346 345 ad2ant2rl vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol * c
347 341 346 eqeltrd vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol c
348 volun a dom vol c dom vol a c = vol a vol c vol a c = vol a + vol c
349 320 322 331 339 347 348 syl32anc vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol a c = vol a + vol c
350 unmbl a dom vol c dom vol a c dom vol
351 59 117 350 syl2an a Clsd topGen ran . c Clsd topGen ran . a c dom vol
352 mblvol a c dom vol vol a c = vol * a c
353 351 352 syl a Clsd topGen ran . c Clsd topGen ran . vol a c = vol * a c
354 353 ad2antlr vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol a c = vol * a c
355 349 354 eqtr3d vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A vol a + vol c = vol * a c
356 318 355 sylan9eqr vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A u = vol a v = vol c u + v = vol * a c
357 eqtr y = u + v u + v = vol * a c y = vol * a c
358 357 ancoms u + v = vol * a c y = u + v y = vol * a c
359 356 358 sylan vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A u = vol a v = vol c y = u + v y = vol * a c
360 66 122 anim12i a ran . f A c ran . f A a ran . f c ran . f
361 unss a ran . f c ran . f a c ran . f
362 360 361 sylib a ran . f A c ran . f A a c ran . f
363 ovolss a c ran . f ran . f vol * a c vol * ran . f
364 362 16 363 sylancl a ran . f A c ran . f A vol * a c vol * ran . f
365 364 ad3antlr vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A u = vol a v = vol c y = u + v vol * a c vol * ran . f
366 359 365 eqbrtrd vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A u = vol a v = vol c y = u + v y vol * ran . f
367 366 ex vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A u = vol a v = vol c y = u + v y vol * ran . f
368 367 expl vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A c ran . f A u = vol a v = vol c y = u + v y vol * ran . f
369 317 368 syl5bir vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A u = vol a c ran . f A v = vol c y = u + v y vol * ran . f
370 369 rexlimdvva vol * ran . f a Clsd topGen ran . c Clsd topGen ran . a ran . f A u = vol a c ran . f A v = vol c y = u + v y vol * ran . f
371 316 370 syl5bir vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c y = u + v y vol * ran . f
372 371 rexlimdvv vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c y = u + v y vol * ran . f
373 372 alrimiv vol * ran . f y u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c y = u + v y vol * ran . f
374 eqeq1 t = y t = u + v y = u + v
375 374 2rexbidv t = y u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c y = u + v
376 375 ralab y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y vol * ran . f y u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c y = u + v y vol * ran . f
377 373 376 sylibr vol * ran . f y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y vol * ran . f
378 simpr vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v t = u + v
379 74 sselda vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a u
380 130 sselda vol * ran . f v z | c Clsd topGen ran . c ran . f A z = vol c v
381 readdcl u v u + v
382 379 380 381 syl2an vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a vol * ran . f v z | c Clsd topGen ran . c ran . f A z = vol c u + v
383 382 anandis vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c u + v
384 383 adantr vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v u + v
385 378 384 eqeltrd vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v t
386 385 ex vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v t
387 386 rexlimdvva vol * ran . f u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v t
388 387 abssdv vol * ran . f t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v
389 00id 0 + 0 = 0
390 389 eqcomi 0 = 0 + 0
391 rspceov 0 z | a Clsd topGen ran . a ran . f A z = vol a 0 z | c Clsd topGen ran . c ran . f A z = vol c 0 = 0 + 0 u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c 0 = u + v
392 110 157 390 391 mp3an u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c 0 = u + v
393 eqeq1 t = 0 t = u + v 0 = u + v
394 393 2rexbidv t = 0 u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c 0 = u + v
395 105 394 spcev u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c 0 = u + v t u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v
396 392 395 ax-mp t u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v
397 abn0 t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v t u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v
398 396 397 mpbir t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v
399 398 a1i vol * ran . f t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v
400 brralrspcev vol * ran . f y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y vol * ran . f x y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y x
401 377 400 mpdan vol * ran . f x y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y x
402 388 399 401 3jca vol * ran . f t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v x y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y x
403 suprleub t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v x y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y x vol * ran . f sup t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v < vol * ran . f y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y vol * ran . f
404 402 403 mpancom vol * ran . f sup t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v < vol * ran . f y t | u z | a Clsd topGen ran . a ran . f A z = vol a v z | c Clsd topGen ran . c ran . f A z = vol c t = u + v y vol * ran . f
405 377 404 mpbird vol * ran . f sup t | u z | a Clsd topGen ran . a