Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2split Structured version   Unicode version

Theorem itg2split 19644
 Description: The integral splits under an almost disjoint union. (The proof avoids the use of itg2add 19654 which requires CC.) (Contributed by Mario Carneiro, 11-Aug-2014.)
Hypotheses
Ref Expression
itg2split.a
itg2split.b
itg2split.i
itg2split.u
itg2split.c
itg2split.f
itg2split.g
itg2split.h
itg2split.sf
itg2split.sg
Assertion
Ref Expression
itg2split
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem itg2split
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg2split.a . . 3
2 itg2split.b . . 3
3 itg2split.i . . 3
4 itg2split.u . . 3
5 itg2split.c . . 3
6 itg2split.f . . 3
7 itg2split.g . . 3
8 itg2split.h . . 3
9 itg2split.sf . . 3
10 itg2split.sg . . 3
111, 2, 3, 4, 5, 6, 7, 8, 9, 10itg2splitlem 19643 . 2
1210adantr 453 . . . . . . 7
135adantlr 697 . . . . . . . . . . 11
14 0xr 9136 . . . . . . . . . . . . 13
15 0le0 10086 . . . . . . . . . . . . 13
16 elxrge0 11013 . . . . . . . . . . . . 13
1714, 15, 16mpbir2an 888 . . . . . . . . . . . 12
1817a1i 11 . . . . . . . . . . 11
1913, 18ifclda 3768 . . . . . . . . . 10
2019, 8fmptd 5896 . . . . . . . . 9
219, 10readdcld 9120 . . . . . . . . 9
22 itg2lecl 19633 . . . . . . . . 9
2320, 21, 11, 22syl3anc 1185 . . . . . . . 8
2423adantr 453 . . . . . . 7
25 itg1cl 19580 . . . . . . . 8
2625ad2antrl 710 . . . . . . 7
27 simprll 740 . . . . . . . . . . . . . 14
28 simprrl 742 . . . . . . . . . . . . . 14
2927, 28itg1add 19596 . . . . . . . . . . . . 13
3020adantr 453 . . . . . . . . . . . . . 14
3127, 28i1fadd 19590 . . . . . . . . . . . . . 14
32 inss1 3563 . . . . . . . . . . . . . . . 16
33 mblss 19432 . . . . . . . . . . . . . . . . 17
341, 33syl 16 . . . . . . . . . . . . . . . 16
3532, 34syl5ss 3361 . . . . . . . . . . . . . . 15
3635adantr 453 . . . . . . . . . . . . . 14
373adantr 453 . . . . . . . . . . . . . 14
38 nfv 1630 . . . . . . . . . . . . . . . . . 18
39 nfv 1630 . . . . . . . . . . . . . . . . . . . 20
40 nfcv 2574 . . . . . . . . . . . . . . . . . . . . 21
41 nfcv 2574 . . . . . . . . . . . . . . . . . . . . 21
42 nfmpt1 4301 . . . . . . . . . . . . . . . . . . . . . 22
436, 42nfcxfr 2571 . . . . . . . . . . . . . . . . . . . . 21
4440, 41, 43nfbr 4259 . . . . . . . . . . . . . . . . . . . 20
4539, 44nfan 1847 . . . . . . . . . . . . . . . . . . 19
46 nfv 1630 . . . . . . . . . . . . . . . . . . . 20
47 nfcv 2574 . . . . . . . . . . . . . . . . . . . . 21
48 nfmpt1 4301 . . . . . . . . . . . . . . . . . . . . . 22
497, 48nfcxfr 2571 . . . . . . . . . . . . . . . . . . . . 21
5047, 41, 49nfbr 4259 . . . . . . . . . . . . . . . . . . . 20
5146, 50nfan 1847 . . . . . . . . . . . . . . . . . . 19
5245, 51nfan 1847 . . . . . . . . . . . . . . . . . 18
5338, 52nfan 1847 . . . . . . . . . . . . . . . . 17
54 eldifi 3471 . . . . . . . . . . . . . . . . . . . 20
55 i1ff 19571 . . . . . . . . . . . . . . . . . . . . . . 23
5627, 55syl 16 . . . . . . . . . . . . . . . . . . . . . 22
57 ffn 5594 . . . . . . . . . . . . . . . . . . . . . 22
5856, 57syl 16 . . . . . . . . . . . . . . . . . . . . 21
59 i1ff 19571 . . . . . . . . . . . . . . . . . . . . . . 23
6028, 59syl 16 . . . . . . . . . . . . . . . . . . . . . 22
61 ffn 5594 . . . . . . . . . . . . . . . . . . . . . 22
6260, 61syl 16 . . . . . . . . . . . . . . . . . . . . 21
63 reex 9086 . . . . . . . . . . . . . . . . . . . . . 22
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21
65 inidm 3552 . . . . . . . . . . . . . . . . . . . . 21
66 eqidd 2439 . . . . . . . . . . . . . . . . . . . . 21
67 eqidd 2439 . . . . . . . . . . . . . . . . . . . . 21
6858, 62, 64, 64, 65, 66, 67ofval 6317 . . . . . . . . . . . . . . . . . . . 20
6954, 68sylan2 462 . . . . . . . . . . . . . . . . . . 19
70 ffvelrn 5871 . . . . . . . . . . . . . . . . . . . . . . . . 25
7156, 54, 70syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . 24
72 ffvelrn 5871 . . . . . . . . . . . . . . . . . . . . . . . . 25
7360, 54, 72syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . 24
7471, 73readdcld 9120 . . . . . . . . . . . . . . . . . . . . . . 23
7574rexrd 9139 . . . . . . . . . . . . . . . . . . . . . 22
7675adantr 453 . . . . . . . . . . . . . . . . . . . . 21
7771adantr 453 . . . . . . . . . . . . . . . . . . . . . 22
7877rexrd 9139 . . . . . . . . . . . . . . . . . . . . 21
79 iccssxr 10998 . . . . . . . . . . . . . . . . . . . . . . 23
80 ffvelrn 5871 . . . . . . . . . . . . . . . . . . . . . . . 24
8130, 54, 80syl2an 465 . . . . . . . . . . . . . . . . . . . . . . 23
8279, 81sseldi 3348 . . . . . . . . . . . . . . . . . . . . . 22
8382adantr 453 . . . . . . . . . . . . . . . . . . . . 21
8473adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
85 0re 9096 . . . . . . . . . . . . . . . . . . . . . . . 24
8685a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
87 simprrr 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8863a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
89 fvex 5745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9089a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
91 ssun2 3513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9291, 4syl5sseqr 3399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9392sselda 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9493adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9594, 13syldan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9617a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9795, 96ifclda 3768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9897adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
99 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
100 dffn5 5775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
10199, 100sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1027a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10388, 90, 98, 101, 102ofrfval2 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10462, 103syldan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10587, 104mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
106105r19.21bi 2806 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10754, 106sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . 25
108107adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24
109 eldifn 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
110109adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111 elin 3532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
112110, 111sylnib 297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
113 imnan 413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
114112, 113sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . 26
115114imp 420 . . . . . . . . . . . . . . . . . . . . . . . . 25
116 iffalse 3748 . . . . . . . . . . . . . . . . . . . . . . . . 25
117115, 116syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
118108, 117breqtrd 4239 . . . . . . . . . . . . . . . . . . . . . . 23
11984, 86, 77, 118leadd2dd 9646 . . . . . . . . . . . . . . . . . . . . . 22
12077recnd 9119 . . . . . . . . . . . . . . . . . . . . . . 23
121120addid1d 9271 . . . . . . . . . . . . . . . . . . . . . 22
122119, 121breqtrd 4239 . . . . . . . . . . . . . . . . . . . . 21
123 simprlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . 26
12463a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125 fvex 5745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126125a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127 ssun1 3512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
128127, 4syl5sseqr 3399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
129128sselda 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
130129adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
131130, 13syldan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
13217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133131, 132ifclda 3768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
134133adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
135 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136 dffn5 5775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137135, 136sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1386a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
139124, 126, 134, 137, 138ofrfval2 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
14058, 139syldan 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26
141123, 140mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . 25
142141r19.21bi 2806 . . . . . . . . . . . . . . . . . . . . . . . 24
14354, 142sylan2 462 . . . . . . . . . . . . . . . . . . . . . . 23
144143adantr 453 . . . . . . . . . . . . . . . . . . . . . 22
145128ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25
146145sselda 3350 . . . . . . . . . . . . . . . . . . . . . . . 24
147 iftrue 3747 . . . . . . . . . . . . . . . . . . . . . . . 24
148146, 147syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
149 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26
15019adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1518fvmpt2 5815 . . . . . . . . . . . . . . . . . . . . . . . . . 26
152149, 150, 151syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . 25
15354, 152sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . 24
154153adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
155 iftrue 3747 . . . . . . . . . . . . . . . . . . . . . . . 24
156155adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23
157148, 154, 1563eqtr4d 2480 . . . . . . . . . . . . . . . . . . . . . 22
158144, 157breqtrrd 4241 . . . . . . . . . . . . . . . . . . . . 21
15976, 78, 83, 122, 158xrletrd 10757 . . . . . . . . . . . . . . . . . . . 20
16075adantr 453 . . . . . . . . . . . . . . . . . . . . 21
16173adantr 453 . . . . . . . . . . . . . . . . . . . . . 22
162161rexrd 9139 . . . . . . . . . . . . . . . . . . . . 21
16382adantr 453 . . . . . . . . . . . . . . . . . . . . 21
16471adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
16585a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
166143adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24
167 iffalse 3748 . . . . . . . . . . . . . . . . . . . . . . . . 25
168167adantl 454 . . . . . . . . . . . . . . . . . . . . . . . 24
169166, 168breqtrd 4239 . . . . . . . . . . . . . . . . . . . . . . 23
170164, 165, 161, 169leadd1dd 9645 . . . . . . . . . . . . . . . . . . . . . 22
171161recnd 9119 . . . . . . . . . . . . . . . . . . . . . . 23
172171addid2d 9272 . . . . . . . . . . . . . . . . . . . . . 22
173170, 172breqtrd 4239 . . . . . . . . . . . . . . . . . . . . 21
174107adantr 453 . . . . . . . . . . . . . . . . . . . . . 22
175153adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
1764ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26
177176eleq2d 2505 . . . . . . . . . . . . . . . . . . . . . . . . 25
178 biorf 396 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
179 elun 3490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
180178, 179syl6rbbr 257 . . . . . . . . . . . . . . . . . . . . . . . . . 26
181180adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . 25
182177, 181bitrd 246 . . . . . . . . . . . . . . . . . . . . . . . 24
183182ifbid 3759 . . . . . . . . . . . . . . . . . . . . . . 23
184175, 183eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . 22
185174, 184breqtrrd 4241 . . . . . . . . . . . . . . . . . . . . 21
186160, 162, 163, 173, 185xrletrd 10757 . . . . . . . . . . . . . . . . . . . 20
187159, 186pm2.61dan 768 . . . . . . . . . . . . . . . . . . 19
18869, 187eqbrtrd 4235 . . . . . . . . . . . . . . . . . 18
189188ex 425 . . . . . . . . . . . . . . . . 17
19053, 189ralrimi 2789 . . . . . . . . . . . . . . . 16
191 nfv 1630 . . . . . . . . . . . . . . . . 17
192 nfcv 2574 . . . . . . . . . . . . . . . . . 18
193 nfcv 2574 . . . . . . . . . . . . . . . . . 18
194 nfmpt1 4301 . . . . . . . . . . . . . . . . . . . 20
1958, 194nfcxfr 2571 . . . . . . . . . . . . . . . . . . 19
196 nfcv 2574 . . . . . . . . . . . . . . . . . . 19
197195, 196nffv 5738 . . . . . . . . . . . . . . . . . 18
198192, 193, 197nfbr 4259 . . . . . . . . . . . . . . . . 17
199 fveq2 5731 . . . . . . . . . . . . . . . . . 18
200 fveq2 5731 . . . . . . . . . . . . . . . . . 18
201199, 200breq12d 4228 . . . . . . . . . . . . . . . . 17
202191, 198, 201cbvral 2930 . . . . . . . . . . . . . . . 16
203190, 202sylib 190 . . . . . . . . . . . . . . 15
204203r19.21bi 2806 . . . . . . . . . . . . . 14
20530, 31, 36, 37, 204itg2uba 19638 . . . . . . . . . . . . 13
20629, 205eqbrtrrd 4237 . . . . . . . . . . . 12
20726adantrr 699 . . . . . . . . . . . . 13
208 itg1cl 19580 . . . . . . . . . . . . . 14
20928, 208syl 16 . . . . . . . . . . . . 13
21023adantr 453 . . . . . . . . . . . . 13
211207, 209, 210leaddsub2d 9633 . . . . . . . . . . . 12
212206, 211mpbid 203 . . . . . . . . . . 11
213212anassrs 631 . . . . . . . . . 10
214213expr 600 . . . . . . . . 9
215214ralrimiva 2791 . . . . . . . 8
21697, 7fmptd 5896 . . . . . . . . . 10
217216adantr 453 . . . . . . . . 9
21824, 26resubcld 9470 . . . . . . . . . 10
219218rexrd 9139 . . . . . . . . 9
220 itg2leub 19629 . . . . . . . . 9
221217, 219, 220syl2anc 644 . . . . . . . 8
222215, 221mpbird 225 . . . . . . 7
22312, 24, 26, 222lesubd 9635 . . . . . 6
224223expr 600 . . . . 5
225224ralrimiva 2791 . . . 4
226133, 6fmptd 5896 . . . . 5
22723, 10resubcld 9470 . . . . . 6
228227rexrd 9139 . . . . 5
229 itg2leub 19629 . . . . 5
230226, 228, 229syl2anc 644 . . . 4
231225, 230mpbird 225 . . 3
232 leaddsub 9509 . . . 4
2339, 10, 23, 232syl3anc 1185 . . 3
234231, 233mpbird 225 . 2
235 itg2cl 19627 . . . 4
23620, 235syl 16 . . 3
23721rexrd 9139 . . 3
238 xrletri3 10750 . . 3
239236, 237, 238syl2anc 644 . 2
24011, 234, 239mpbir2and 890 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wo 359   wa 360   wceq 1653   wcel 1726  wral 2707  cvv 2958   cdif 3319   cun 3320   cin 3321   wss 3322  cif 3741   class class class wbr 4215   cmpt 4269   cdm 4881   wfn 5452  wf 5453  cfv 5457  (class class class)co 6084   cof 6306   cofr 6307  cr 8994  cc0 8995   caddc 8998   cpnf 9122  cxr 9124   cle 9126   cmin 9296  cicc 10924  covol 19364  cvol 19365  citg1 19512  citg2 19513 This theorem is referenced by:  itg2cnlem2  19657  itgsplit  19730 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072  ax-pre-sup 9073  ax-addf 9074 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-disj 4186  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6308  df-ofr 6309  df-1st 6352  df-2nd 6353  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-map 7023  df-pm 7024  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-fi 7419  df-sup 7449  df-oi 7482  df-card 7831  df-cda 8053  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-div 9683  df-nn 10006  df-2 10063  df-3 10064  df-n0 10227  df-z 10288  df-uz 10494  df-q 10580  df-rp 10618  df-xneg 10715  df-xadd 10716  df-xmul 10717  df-ioo 10925  df-ico 10927  df-icc 10928  df-fz 11049  df-fzo 11141  df-fl 11207  df-seq 11329  df-exp 11388  df-hash 11624  df-cj 11909  df-re 11910  df-im 11911  df-sqr 12045  df-abs 12046  df-clim 12287  df-sum 12485  df-rest 13655  df-topgen 13672  df-psmet 16699  df-xmet 16700  df-met 16701  df-bl 16702  df-mopn 16703  df-top 16968  df-bases 16970  df-topon 16971  df-cmp 17455  df-ovol 19366  df-vol 19367  df-mbf 19516  df-itg1 19517  df-itg2 19518
 Copyright terms: Public domain W3C validator