Metamath Proof Explorer


Theorem itgsplit

Description: The S. integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgsplit.i φvol*AB=0
itgsplit.u φU=AB
itgsplit.c φxUCV
itgsplit.a φxAC𝐿1
itgsplit.b φxBC𝐿1
Assertion itgsplit φUCdx=ACdx+BCdx

Proof

Step Hyp Ref Expression
1 itgsplit.i φvol*AB=0
2 itgsplit.u φU=AB
3 itgsplit.c φxUCV
4 itgsplit.a φxAC𝐿1
5 itgsplit.b φxBC𝐿1
6 iblmbf xAC𝐿1xACMblFn
7 4 6 syl φxACMblFn
8 ssun1 AAB
9 8 2 sseqtrrid φAU
10 9 sselda φxAxU
11 10 3 syldan φxACV
12 7 11 mbfdm2 φAdomvol
13 12 adantr φk03Adomvol
14 iblmbf xBC𝐿1xBCMblFn
15 5 14 syl φxBCMblFn
16 ssun2 BAB
17 16 2 sseqtrrid φBU
18 17 sselda φxBxU
19 18 3 syldan φxBCV
20 15 19 mbfdm2 φBdomvol
21 20 adantr φk03Bdomvol
22 1 adantr φk03vol*AB=0
23 2 adantr φk03U=AB
24 2 eleq2d φxUxAB
25 elun xABxAxB
26 24 25 bitrdi φxUxAxB
27 26 biimpa φxUxAxB
28 7 11 mbfmptcl φxAC
29 15 19 mbfmptcl φxBC
30 28 29 jaodan φxAxBC
31 27 30 syldan φxUC
32 31 adantlr φk03xUC
33 ax-icn i
34 elfznn0 k03k0
35 34 adantl φk03k0
36 expcl ik0ik
37 33 35 36 sylancr φk03ik
38 37 adantr φk03xUik
39 ine0 i0
40 elfzelz k03k
41 40 adantl φk03k
42 expne0i ii0kik0
43 33 39 41 42 mp3an12i φk03ik0
44 43 adantr φk03xUik0
45 32 38 44 divcld φk03xUCik
46 45 recld φk03xUCik
47 0re 0
48 ifcl Cik0if0CikCik0
49 46 47 48 sylancl φk03xUif0CikCik0
50 49 rexrd φk03xUif0CikCik0*
51 max1 0Cik0if0CikCik0
52 47 46 51 sylancr φk03xU0if0CikCik0
53 elxrge0 if0CikCik00+∞if0CikCik0*0if0CikCik0
54 50 52 53 sylanbrc φk03xUif0CikCik00+∞
55 ifan ifxA0CikCik0=ifxAif0CikCik00
56 55 mpteq2i xifxA0CikCik0=xifxAif0CikCik00
57 ifan ifxB0CikCik0=ifxBif0CikCik00
58 57 mpteq2i xifxB0CikCik0=xifxBif0CikCik00
59 ifan ifxU0CikCik0=ifxUif0CikCik00
60 59 mpteq2i xifxU0CikCik0=xifxUif0CikCik00
61 eqidd φxifxA0CikCik0=xifxA0CikCik0
62 eqidd φxACik=Cik
63 61 62 4 11 iblitg φk2xifxA0CikCik0
64 40 63 sylan2 φk032xifxA0CikCik0
65 eqidd φxifxB0CikCik0=xifxB0CikCik0
66 eqidd φxBCik=Cik
67 65 66 5 19 iblitg φk2xifxB0CikCik0
68 40 67 sylan2 φk032xifxB0CikCik0
69 13 21 22 23 54 56 58 60 64 68 itg2split φk032xifxU0CikCik0=2xifxA0CikCik0+2xifxB0CikCik0
70 69 oveq2d φk03ik2xifxU0CikCik0=ik2xifxA0CikCik0+2xifxB0CikCik0
71 63 recnd φk2xifxA0CikCik0
72 40 71 sylan2 φk032xifxA0CikCik0
73 68 recnd φk032xifxB0CikCik0
74 37 72 73 adddid φk03ik2xifxA0CikCik0+2xifxB0CikCik0=ik2xifxA0CikCik0+ik2xifxB0CikCik0
75 70 74 eqtrd φk03ik2xifxU0CikCik0=ik2xifxA0CikCik0+ik2xifxB0CikCik0
76 75 sumeq2dv φk=03ik2xifxU0CikCik0=k=03ik2xifxA0CikCik0+ik2xifxB0CikCik0
77 fzfid φ03Fin
78 37 72 mulcld φk03ik2xifxA0CikCik0
79 37 73 mulcld φk03ik2xifxB0CikCik0
80 77 78 79 fsumadd φk=03ik2xifxA0CikCik0+ik2xifxB0CikCik0=k=03ik2xifxA0CikCik0+k=03ik2xifxB0CikCik0
81 76 80 eqtrd φk=03ik2xifxU0CikCik0=k=03ik2xifxA0CikCik0+k=03ik2xifxB0CikCik0
82 eqid Cik=Cik
83 82 dfitg UCdx=k=03ik2xifxU0CikCik0
84 82 dfitg ACdx=k=03ik2xifxA0CikCik0
85 82 dfitg BCdx=k=03ik2xifxB0CikCik0
86 84 85 oveq12i ACdx+BCdx=k=03ik2xifxA0CikCik0+k=03ik2xifxB0CikCik0
87 81 83 86 3eqtr4g φUCdx=ACdx+BCdx