Metamath Proof Explorer


Theorem itgsplitioo

Description: The S. integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgsplitioo.1 φA
itgsplitioo.2 φC
itgsplitioo.3 φBAC
itgsplitioo.4 φxACD
itgsplitioo.5 φxABD𝐿1
itgsplitioo.6 φxBCD𝐿1
Assertion itgsplitioo φACDdx=ABDdx+BCDdx

Proof

Step Hyp Ref Expression
1 itgsplitioo.1 φA
2 itgsplitioo.2 φC
3 itgsplitioo.3 φBAC
4 itgsplitioo.4 φxACD
5 itgsplitioo.5 φxABD𝐿1
6 itgsplitioo.6 φxBCD𝐿1
7 elicc2 ACBACBABBC
8 1 2 7 syl2anc φBACBABBC
9 3 8 mpbid φBABBC
10 9 simp2d φAB
11 9 simp1d φB
12 1 11 leloed φABA<BA=B
13 10 12 mpbid φA<BA=B
14 13 ord φ¬A<BA=B
15 1 rexrd φA*
16 iooss1 A*ABBCAC
17 15 10 16 syl2anc φBCAC
18 17 sselda φxBCxAC
19 18 4 syldan φxBCD
20 19 6 itgcl φBCDdx
21 20 addid2d φ0+BCDdx=BCDdx
22 21 eqcomd φBCDdx=0+BCDdx
23 oveq1 A=BAC=BC
24 itgeq1 AC=BCACDdx=BCDdx
25 23 24 syl A=BACDdx=BCDdx
26 oveq1 A=BAB=BB
27 iooid BB=
28 26 27 eqtrdi A=BAB=
29 itgeq1 AB=ABDdx=Ddx
30 28 29 syl A=BABDdx=Ddx
31 itg0 Ddx=0
32 30 31 eqtrdi A=BABDdx=0
33 32 oveq1d A=BABDdx+BCDdx=0+BCDdx
34 25 33 eqeq12d A=BACDdx=ABDdx+BCDdxBCDdx=0+BCDdx
35 22 34 syl5ibrcom φA=BACDdx=ABDdx+BCDdx
36 14 35 syld φ¬A<BACDdx=ABDdx+BCDdx
37 9 simp3d φBC
38 11 2 leloed φBCB<CB=C
39 37 38 mpbid φB<CB=C
40 39 ord φ¬B<CB=C
41 2 rexrd φC*
42 iooss2 C*BCABAC
43 41 37 42 syl2anc φABAC
44 43 sselda φxABxAC
45 44 4 syldan φxABD
46 45 5 itgcl φABDdx
47 46 addid1d φABDdx+0=ABDdx
48 47 eqcomd φABDdx=ABDdx+0
49 oveq2 B=CAB=AC
50 itgeq1 AB=ACABDdx=ACDdx
51 49 50 syl B=CABDdx=ACDdx
52 oveq2 B=CBB=BC
53 27 52 eqtr3id B=C=BC
54 itgeq1 =BCDdx=BCDdx
55 53 54 syl B=CDdx=BCDdx
56 31 55 eqtr3id B=C0=BCDdx
57 56 oveq2d B=CABDdx+0=ABDdx+BCDdx
58 51 57 eqeq12d B=CABDdx=ABDdx+0ACDdx=ABDdx+BCDdx
59 48 58 syl5ibcom φB=CACDdx=ABDdx+BCDdx
60 40 59 syld φ¬B<CACDdx=ABDdx+BCDdx
61 indir ABBBC=ABBCBBC
62 11 rexrd φB*
63 15 62 jca φA*B*
64 63 adantr φA<BB<CA*B*
65 62 41 jca φB*C*
66 65 adantr φA<BB<CB*C*
67 11 adantr φA<BB<CB
68 67 leidd φA<BB<CBB
69 ioodisj A*B*B*C*BBABBC=
70 64 66 68 69 syl21anc φA<BB<CABBC=
71 incom BBC=BCB
72 67 ltnrd φA<BB<C¬B<B
73 eliooord BBCB<BB<C
74 73 simpld BBCB<B
75 72 74 nsyl φA<BB<C¬BBC
76 disjsn BCB=¬BBC
77 75 76 sylibr φA<BB<CBCB=
78 71 77 eqtrid φA<BB<CBBC=
79 70 78 uneq12d φA<BB<CABBCBBC=
80 un0 =
81 79 80 eqtrdi φA<BB<CABBCBBC=
82 61 81 eqtrid φA<BB<CABBBC=
83 82 fveq2d φA<BB<Cvol*ABBBC=vol*
84 ovol0 vol*=0
85 83 84 eqtrdi φA<BB<Cvol*ABBBC=0
86 15 62 41 3jca φA*B*C*
87 ioojoin A*B*C*A<BB<CABBBC=AC
88 86 87 sylan φA<BB<CABBBC=AC
89 88 eqcomd φA<BB<CAC=ABBBC
90 4 adantlr φA<BB<CxACD
91 5 adantr φA<BB<CxABD𝐿1
92 ssun1 ABABB
93 92 a1i φA<BB<CABABB
94 ioossre AB
95 94 a1i φA<BB<CAB
96 67 snssd φA<BB<CB
97 95 96 unssd φA<BB<CABB
98 uncom ABB=BAB
99 98 difeq1i ABBAB=BABAB
100 difun2 BABAB=BAB
101 99 100 eqtri ABBAB=BAB
102 difss BABB
103 101 102 eqsstri ABBABB
104 ovolsn Bvol*B=0
105 67 104 syl φA<BB<Cvol*B=0
106 ovolssnul ABBABBBvol*B=0vol*ABBAB=0
107 103 96 105 106 mp3an2i φA<BB<Cvol*ABBAB=0
108 ssun1 ABBABBBC
109 108 88 sseqtrid φA<BB<CABBAC
110 109 sselda φA<BB<CxABBxAC
111 110 90 syldan φA<BB<CxABBD
112 93 97 107 111 itgss3 φA<BB<CxABD𝐿1xABBD𝐿1ABDdx=ABBDdx
113 112 simpld φA<BB<CxABD𝐿1xABBD𝐿1
114 91 113 mpbid φA<BB<CxABBD𝐿1
115 6 adantr φA<BB<CxBCD𝐿1
116 85 89 90 114 115 itgsplit φA<BB<CACDdx=ABBDdx+BCDdx
117 112 simprd φA<BB<CABDdx=ABBDdx
118 117 oveq1d φA<BB<CABDdx+BCDdx=ABBDdx+BCDdx
119 116 118 eqtr4d φA<BB<CACDdx=ABDdx+BCDdx
120 119 ex φA<BB<CACDdx=ABDdx+BCDdx
121 36 60 120 ecased φACDdx=ABDdx+BCDdx