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

Theorem itg2split 22786
 Description: The integral splits under an almost disjoint union. (The proof avoids the use of itg2add 22796 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 22785 . 2
1210adantr 472 . . . . . . 7
135adantlr 729 . . . . . . . . . . 11
14 0e0iccpnf 11769 . . . . . . . . . . . 12
1514a1i 11 . . . . . . . . . . 11
1613, 15ifclda 3904 . . . . . . . . . 10
1716, 8fmptd 6061 . . . . . . . . 9
189, 10readdcld 9688 . . . . . . . . 9
19 itg2lecl 22775 . . . . . . . . 9
2017, 18, 11, 19syl3anc 1292 . . . . . . . 8
2120adantr 472 . . . . . . 7
22 itg1cl 22722 . . . . . . . 8
2322ad2antrl 742 . . . . . . 7
24 simprll 780 . . . . . . . . . . . . . 14
25 simprrl 782 . . . . . . . . . . . . . 14
2624, 25itg1add 22738 . . . . . . . . . . . . 13
2717adantr 472 . . . . . . . . . . . . . 14
2824, 25i1fadd 22732 . . . . . . . . . . . . . 14
29 inss1 3643 . . . . . . . . . . . . . . . 16
30 mblss 22563 . . . . . . . . . . . . . . . . 17
311, 30syl 17 . . . . . . . . . . . . . . . 16
3229, 31syl5ss 3429 . . . . . . . . . . . . . . 15
3332adantr 472 . . . . . . . . . . . . . 14
343adantr 472 . . . . . . . . . . . . . 14
35 nfv 1769 . . . . . . . . . . . . . . . . . 18
36 nfv 1769 . . . . . . . . . . . . . . . . . . . 20
37 nfcv 2612 . . . . . . . . . . . . . . . . . . . . 21
38 nfcv 2612 . . . . . . . . . . . . . . . . . . . . 21
39 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . . . 22
406, 39nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . 21
4137, 38, 40nfbr 4440 . . . . . . . . . . . . . . . . . . . 20
4236, 41nfan 2031 . . . . . . . . . . . . . . . . . . 19
43 nfv 1769 . . . . . . . . . . . . . . . . . . . 20
44 nfcv 2612 . . . . . . . . . . . . . . . . . . . . 21
45 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . . . 22
467, 45nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . 21
4744, 38, 46nfbr 4440 . . . . . . . . . . . . . . . . . . . 20
4843, 47nfan 2031 . . . . . . . . . . . . . . . . . . 19
4942, 48nfan 2031 . . . . . . . . . . . . . . . . . 18
5035, 49nfan 2031 . . . . . . . . . . . . . . . . 17
51 eldifi 3544 . . . . . . . . . . . . . . . . . . . 20
52 i1ff 22713 . . . . . . . . . . . . . . . . . . . . . . 23
5324, 52syl 17 . . . . . . . . . . . . . . . . . . . . . 22
54 ffn 5739 . . . . . . . . . . . . . . . . . . . . . 22
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . . 21
56 i1ff 22713 . . . . . . . . . . . . . . . . . . . . . . 23
5725, 56syl 17 . . . . . . . . . . . . . . . . . . . . . 22
58 ffn 5739 . . . . . . . . . . . . . . . . . . . . . 22
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . 21
60 reex 9648 . . . . . . . . . . . . . . . . . . . . . 22
6160a1i 11 . . . . . . . . . . . . . . . . . . . . 21
62 inidm 3632 . . . . . . . . . . . . . . . . . . . . 21
63 eqidd 2472 . . . . . . . . . . . . . . . . . . . . 21
64 eqidd 2472 . . . . . . . . . . . . . . . . . . . . 21
6555, 59, 61, 61, 62, 63, 64ofval 6559 . . . . . . . . . . . . . . . . . . . 20
6651, 65sylan2 482 . . . . . . . . . . . . . . . . . . 19
67 ffvelrn 6035 . . . . . . . . . . . . . . . . . . . . . . . . 25
6853, 51, 67syl2an 485 . . . . . . . . . . . . . . . . . . . . . . . 24
69 ffvelrn 6035 . . . . . . . . . . . . . . . . . . . . . . . . 25
7057, 51, 69syl2an 485 . . . . . . . . . . . . . . . . . . . . . . . 24
7168, 70readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . 23
7271rexrd 9708 . . . . . . . . . . . . . . . . . . . . . 22
7372adantr 472 . . . . . . . . . . . . . . . . . . . . 21
7468adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
7574rexrd 9708 . . . . . . . . . . . . . . . . . . . . 21
76 iccssxr 11742 . . . . . . . . . . . . . . . . . . . . . . 23
77 ffvelrn 6035 . . . . . . . . . . . . . . . . . . . . . . . 24
7827, 51, 77syl2an 485 . . . . . . . . . . . . . . . . . . . . . . 23
7976, 78sseldi 3416 . . . . . . . . . . . . . . . . . . . . . 22
8079adantr 472 . . . . . . . . . . . . . . . . . . . . 21
8170adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
82 0red 9662 . . . . . . . . . . . . . . . . . . . . . . 23
83 simprrr 783 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8460a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
85 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8685a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
87 ssun2 3589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
8887, 4syl5sseqr 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8988sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9089adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9190, 13syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9214a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9391, 92ifclda 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9493adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
95 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
96 dffn5 5924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9795, 96sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
987a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9984, 86, 94, 97, 98ofrfval2 6568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10059, 99syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10183, 100mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
102101r19.21bi 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10351, 102sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . 25
104103adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
105 eldifn 3545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
106105adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
107 elin 3608 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
108106, 107sylnib 311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
109 imnan 429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
110108, 109sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26
111110imp 436 . . . . . . . . . . . . . . . . . . . . . . . . 25
112111iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . 24
113104, 112breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . 23
11481, 82, 74, 113leadd2dd 10249 . . . . . . . . . . . . . . . . . . . . . 22
11574recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
116115addid1d 9851 . . . . . . . . . . . . . . . . . . . . . 22
117114, 116breqtrd 4420 . . . . . . . . . . . . . . . . . . . . 21
118 simprlr 781 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11960a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
120 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122 ssun1 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
123122, 4syl5sseqr 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124123sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125124adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126125, 13syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
12714a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128126, 127ifclda 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
129128adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
130 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
131 dffn5 5924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132130, 131sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1336a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134119, 121, 129, 132, 133ofrfval2 6568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
13555, 134syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . 26
136118, 135mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . 25
137136r19.21bi 2776 . . . . . . . . . . . . . . . . . . . . . . . 24
13851, 137sylan2 482 . . . . . . . . . . . . . . . . . . . . . . 23
139138adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
140123ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
141140sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . 24
142141iftrued 3880 . . . . . . . . . . . . . . . . . . . . . . 23
143 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26
14416adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1458fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . . . 26
146143, 144, 145syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25
14751, 146sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . 24
148147adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
149 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . . 24
150149adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23
151142, 148, 1503eqtr4d 2515 . . . . . . . . . . . . . . . . . . . . . 22
152139, 151breqtrrd 4422 . . . . . . . . . . . . . . . . . . . . 21
15373, 75, 80, 117, 152xrletrd 11482 . . . . . . . . . . . . . . . . . . . 20
15472adantr 472 . . . . . . . . . . . . . . . . . . . . 21
15570adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
156155rexrd 9708 . . . . . . . . . . . . . . . . . . . . 21
15779adantr 472 . . . . . . . . . . . . . . . . . . . . 21
15868adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
159 0red 9662 . . . . . . . . . . . . . . . . . . . . . . 23
160138adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
161 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . . . 25
162161adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24
163160, 162breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . 23
164158, 159, 155, 163leadd1dd 10248 . . . . . . . . . . . . . . . . . . . . . 22
165155recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
166165addid2d 9852 . . . . . . . . . . . . . . . . . . . . . 22
167164, 166breqtrd 4420 . . . . . . . . . . . . . . . . . . . . 21
168103adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
169147adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
1704ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . . . 26
171170eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . . 25
172 biorf 412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
173 elun 3565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
174172, 173syl6rbbr 272 . . . . . . . . . . . . . . . . . . . . . . . . . 26
175174adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25
176171, 175bitrd 261 . . . . . . . . . . . . . . . . . . . . . . . 24
177176ifbid 3894 . . . . . . . . . . . . . . . . . . . . . . 23
178169, 177eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . 22
179168, 178breqtrrd 4422 . . . . . . . . . . . . . . . . . . . . 21
180154, 156, 157, 167, 179xrletrd 11482 . . . . . . . . . . . . . . . . . . . 20
181153, 180pm2.61dan 808 . . . . . . . . . . . . . . . . . . 19
18266, 181eqbrtrd 4416 . . . . . . . . . . . . . . . . . 18
183182ex 441 . . . . . . . . . . . . . . . . 17
18450, 183ralrimi 2800 . . . . . . . . . . . . . . . 16
185 nfv 1769 . . . . . . . . . . . . . . . . 17
186 nfcv 2612 . . . . . . . . . . . . . . . . . 18
187 nfcv 2612 . . . . . . . . . . . . . . . . . 18
188 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . 20
1898, 188nfcxfr 2610 . . . . . . . . . . . . . . . . . . 19
190 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
191189, 190nffv 5886 . . . . . . . . . . . . . . . . . 18
192186, 187, 191nfbr 4440 . . . . . . . . . . . . . . . . 17
193 fveq2 5879 . . . . . . . . . . . . . . . . . 18
194 fveq2 5879 . . . . . . . . . . . . . . . . . 18
195193, 194breq12d 4408 . . . . . . . . . . . . . . . . 17
196185, 192, 195cbvral 3001 . . . . . . . . . . . . . . . 16
197184, 196sylib 201 . . . . . . . . . . . . . . 15
198197r19.21bi 2776 . . . . . . . . . . . . . 14
19927, 28, 33, 34, 198itg2uba 22780 . . . . . . . . . . . . 13
20026, 199eqbrtrrd 4418 . . . . . . . . . . . 12
20123adantrr 731 . . . . . . . . . . . . 13
202 itg1cl 22722 . . . . . . . . . . . . . 14
20325, 202syl 17 . . . . . . . . . . . . 13
20420adantr 472 . . . . . . . . . . . . 13
205201, 203, 204leaddsub2d 10236 . . . . . . . . . . . 12
206200, 205mpbid 215 . . . . . . . . . . 11
207206anassrs 660 . . . . . . . . . 10
208207expr 626 . . . . . . . . 9
209208ralrimiva 2809 . . . . . . . 8
21093, 7fmptd 6061 . . . . . . . . . 10
211210adantr 472 . . . . . . . . 9
21221, 23resubcld 10068 . . . . . . . . . 10
213212rexrd 9708 . . . . . . . . 9
214 itg2leub 22771 . . . . . . . . 9
215211, 213, 214syl2anc 673 . . . . . . . 8
216209, 215mpbird 240 . . . . . . 7
21712, 21, 23, 216lesubd 10238 . . . . . 6
218217expr 626 . . . . 5
219218ralrimiva 2809 . . . 4
220128, 6fmptd 6061 . . . . 5
22120, 10resubcld 10068 . . . . . 6
222221rexrd 9708 . . . . 5
223 itg2leub 22771 . . . . 5
224220, 222, 223syl2anc 673 . . . 4
225219, 224mpbird 240 . . 3
226 leaddsub 10111 . . . 4
2279, 10, 20, 226syl3anc 1292 . . 3
228225, 227mpbird 240 . 2
229 itg2cl 22769 . . . 4
23017, 229syl 17 . . 3
23118rexrd 9708 . . 3
232 xrletri3 11474 . . 3
233230, 231, 232syl2anc 673 . 2
23411, 228, 233mpbir2and 936 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   wceq 1452   wcel 1904  wral 2756  cvv 3031   cdif 3387   cun 3388   cin 3389   wss 3390  cif 3872   class class class wbr 4395   cmpt 4454   cdm 4839   wfn 5584  wf 5585  cfv 5589  (class class class)co 6308   cof 6548   cofr 6549  cr 9556  cc0 9557   caddc 9560   cpnf 9690  cxr 9692   cle 9694   cmin 9880  cicc 11663  covol 22491  cvol 22493  citg1 22652  citg2 22653 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-rest 15399  df-topgen 15420  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-top 19998  df-bases 19999  df-topon 20000  df-cmp 20479  df-ovol 22494  df-vol 22496  df-mbf 22656  df-itg1 22657  df-itg2 22658 This theorem is referenced by:  itg2cnlem2  22799  itgsplit  22872  iblsplit  37940
 Copyright terms: Public domain W3C validator