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
|- ( ph -> A e. RR )
itgsplitioo.2
|- ( ph -> C e. RR )
itgsplitioo.3
|- ( ph -> B e. ( A [,] C ) )
itgsplitioo.4
|- ( ( ph /\ x e. ( A (,) C ) ) -> D e. CC )
itgsplitioo.5
|- ( ph -> ( x e. ( A (,) B ) |-> D ) e. L^1 )
itgsplitioo.6
|- ( ph -> ( x e. ( B (,) C ) |-> D ) e. L^1 )
Assertion itgsplitioo
|- ( ph -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) )

Proof

Step Hyp Ref Expression
1 itgsplitioo.1
 |-  ( ph -> A e. RR )
2 itgsplitioo.2
 |-  ( ph -> C e. RR )
3 itgsplitioo.3
 |-  ( ph -> B e. ( A [,] C ) )
4 itgsplitioo.4
 |-  ( ( ph /\ x e. ( A (,) C ) ) -> D e. CC )
5 itgsplitioo.5
 |-  ( ph -> ( x e. ( A (,) B ) |-> D ) e. L^1 )
6 itgsplitioo.6
 |-  ( ph -> ( x e. ( B (,) C ) |-> D ) e. L^1 )
7 elicc2
 |-  ( ( A e. RR /\ C e. RR ) -> ( B e. ( A [,] C ) <-> ( B e. RR /\ A <_ B /\ B <_ C ) ) )
8 1 2 7 syl2anc
 |-  ( ph -> ( B e. ( A [,] C ) <-> ( B e. RR /\ A <_ B /\ B <_ C ) ) )
9 3 8 mpbid
 |-  ( ph -> ( B e. RR /\ A <_ B /\ B <_ C ) )
10 9 simp2d
 |-  ( ph -> A <_ B )
11 9 simp1d
 |-  ( ph -> B e. RR )
12 1 11 leloed
 |-  ( ph -> ( A <_ B <-> ( A < B \/ A = B ) ) )
13 10 12 mpbid
 |-  ( ph -> ( A < B \/ A = B ) )
14 13 ord
 |-  ( ph -> ( -. A < B -> A = B ) )
15 1 rexrd
 |-  ( ph -> A e. RR* )
16 iooss1
 |-  ( ( A e. RR* /\ A <_ B ) -> ( B (,) C ) C_ ( A (,) C ) )
17 15 10 16 syl2anc
 |-  ( ph -> ( B (,) C ) C_ ( A (,) C ) )
18 17 sselda
 |-  ( ( ph /\ x e. ( B (,) C ) ) -> x e. ( A (,) C ) )
19 18 4 syldan
 |-  ( ( ph /\ x e. ( B (,) C ) ) -> D e. CC )
20 19 6 itgcl
 |-  ( ph -> S. ( B (,) C ) D _d x e. CC )
21 20 addid2d
 |-  ( ph -> ( 0 + S. ( B (,) C ) D _d x ) = S. ( B (,) C ) D _d x )
22 21 eqcomd
 |-  ( ph -> S. ( B (,) C ) D _d x = ( 0 + S. ( B (,) C ) D _d x ) )
23 oveq1
 |-  ( A = B -> ( A (,) C ) = ( B (,) C ) )
24 itgeq1
 |-  ( ( A (,) C ) = ( B (,) C ) -> S. ( A (,) C ) D _d x = S. ( B (,) C ) D _d x )
25 23 24 syl
 |-  ( A = B -> S. ( A (,) C ) D _d x = S. ( B (,) C ) D _d x )
26 oveq1
 |-  ( A = B -> ( A (,) B ) = ( B (,) B ) )
27 iooid
 |-  ( B (,) B ) = (/)
28 26 27 eqtrdi
 |-  ( A = B -> ( A (,) B ) = (/) )
29 itgeq1
 |-  ( ( A (,) B ) = (/) -> S. ( A (,) B ) D _d x = S. (/) D _d x )
30 28 29 syl
 |-  ( A = B -> S. ( A (,) B ) D _d x = S. (/) D _d x )
31 itg0
 |-  S. (/) D _d x = 0
32 30 31 eqtrdi
 |-  ( A = B -> S. ( A (,) B ) D _d x = 0 )
33 32 oveq1d
 |-  ( A = B -> ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) = ( 0 + S. ( B (,) C ) D _d x ) )
34 25 33 eqeq12d
 |-  ( A = B -> ( S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) <-> S. ( B (,) C ) D _d x = ( 0 + S. ( B (,) C ) D _d x ) ) )
35 22 34 syl5ibrcom
 |-  ( ph -> ( A = B -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) ) )
36 14 35 syld
 |-  ( ph -> ( -. A < B -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) ) )
37 9 simp3d
 |-  ( ph -> B <_ C )
38 11 2 leloed
 |-  ( ph -> ( B <_ C <-> ( B < C \/ B = C ) ) )
39 37 38 mpbid
 |-  ( ph -> ( B < C \/ B = C ) )
40 39 ord
 |-  ( ph -> ( -. B < C -> B = C ) )
41 2 rexrd
 |-  ( ph -> C e. RR* )
42 iooss2
 |-  ( ( C e. RR* /\ B <_ C ) -> ( A (,) B ) C_ ( A (,) C ) )
43 41 37 42 syl2anc
 |-  ( ph -> ( A (,) B ) C_ ( A (,) C ) )
44 43 sselda
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) C ) )
45 44 4 syldan
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> D e. CC )
46 45 5 itgcl
 |-  ( ph -> S. ( A (,) B ) D _d x e. CC )
47 46 addid1d
 |-  ( ph -> ( S. ( A (,) B ) D _d x + 0 ) = S. ( A (,) B ) D _d x )
48 47 eqcomd
 |-  ( ph -> S. ( A (,) B ) D _d x = ( S. ( A (,) B ) D _d x + 0 ) )
49 oveq2
 |-  ( B = C -> ( A (,) B ) = ( A (,) C ) )
50 itgeq1
 |-  ( ( A (,) B ) = ( A (,) C ) -> S. ( A (,) B ) D _d x = S. ( A (,) C ) D _d x )
51 49 50 syl
 |-  ( B = C -> S. ( A (,) B ) D _d x = S. ( A (,) C ) D _d x )
52 oveq2
 |-  ( B = C -> ( B (,) B ) = ( B (,) C ) )
53 27 52 eqtr3id
 |-  ( B = C -> (/) = ( B (,) C ) )
54 itgeq1
 |-  ( (/) = ( B (,) C ) -> S. (/) D _d x = S. ( B (,) C ) D _d x )
55 53 54 syl
 |-  ( B = C -> S. (/) D _d x = S. ( B (,) C ) D _d x )
56 31 55 eqtr3id
 |-  ( B = C -> 0 = S. ( B (,) C ) D _d x )
57 56 oveq2d
 |-  ( B = C -> ( S. ( A (,) B ) D _d x + 0 ) = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) )
58 51 57 eqeq12d
 |-  ( B = C -> ( S. ( A (,) B ) D _d x = ( S. ( A (,) B ) D _d x + 0 ) <-> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) ) )
59 48 58 syl5ibcom
 |-  ( ph -> ( B = C -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) ) )
60 40 59 syld
 |-  ( ph -> ( -. B < C -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) ) )
61 indir
 |-  ( ( ( A (,) B ) u. { B } ) i^i ( B (,) C ) ) = ( ( ( A (,) B ) i^i ( B (,) C ) ) u. ( { B } i^i ( B (,) C ) ) )
62 11 rexrd
 |-  ( ph -> B e. RR* )
63 15 62 jca
 |-  ( ph -> ( A e. RR* /\ B e. RR* ) )
64 63 adantr
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( A e. RR* /\ B e. RR* ) )
65 62 41 jca
 |-  ( ph -> ( B e. RR* /\ C e. RR* ) )
66 65 adantr
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( B e. RR* /\ C e. RR* ) )
67 11 adantr
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> B e. RR )
68 67 leidd
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> B <_ B )
69 ioodisj
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( B e. RR* /\ C e. RR* ) ) /\ B <_ B ) -> ( ( A (,) B ) i^i ( B (,) C ) ) = (/) )
70 64 66 68 69 syl21anc
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( A (,) B ) i^i ( B (,) C ) ) = (/) )
71 incom
 |-  ( { B } i^i ( B (,) C ) ) = ( ( B (,) C ) i^i { B } )
72 67 ltnrd
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> -. B < B )
73 eliooord
 |-  ( B e. ( B (,) C ) -> ( B < B /\ B < C ) )
74 73 simpld
 |-  ( B e. ( B (,) C ) -> B < B )
75 72 74 nsyl
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> -. B e. ( B (,) C ) )
76 disjsn
 |-  ( ( ( B (,) C ) i^i { B } ) = (/) <-> -. B e. ( B (,) C ) )
77 75 76 sylibr
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( B (,) C ) i^i { B } ) = (/) )
78 71 77 syl5eq
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( { B } i^i ( B (,) C ) ) = (/) )
79 70 78 uneq12d
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) i^i ( B (,) C ) ) u. ( { B } i^i ( B (,) C ) ) ) = ( (/) u. (/) ) )
80 un0
 |-  ( (/) u. (/) ) = (/)
81 79 80 eqtrdi
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) i^i ( B (,) C ) ) u. ( { B } i^i ( B (,) C ) ) ) = (/) )
82 61 81 syl5eq
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) u. { B } ) i^i ( B (,) C ) ) = (/) )
83 82 fveq2d
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( vol* ` ( ( ( A (,) B ) u. { B } ) i^i ( B (,) C ) ) ) = ( vol* ` (/) ) )
84 ovol0
 |-  ( vol* ` (/) ) = 0
85 83 84 eqtrdi
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( vol* ` ( ( ( A (,) B ) u. { B } ) i^i ( B (,) C ) ) ) = 0 )
86 15 62 41 3jca
 |-  ( ph -> ( A e. RR* /\ B e. RR* /\ C e. RR* ) )
87 ioojoin
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) = ( A (,) C ) )
88 86 87 sylan
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) = ( A (,) C ) )
89 88 eqcomd
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( A (,) C ) = ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) ) )
90 4 adantlr
 |-  ( ( ( ph /\ ( A < B /\ B < C ) ) /\ x e. ( A (,) C ) ) -> D e. CC )
91 5 adantr
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( x e. ( A (,) B ) |-> D ) e. L^1 )
92 ssun1
 |-  ( A (,) B ) C_ ( ( A (,) B ) u. { B } )
93 92 a1i
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( A (,) B ) C_ ( ( A (,) B ) u. { B } ) )
94 ioossre
 |-  ( A (,) B ) C_ RR
95 94 a1i
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( A (,) B ) C_ RR )
96 67 snssd
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> { B } C_ RR )
97 95 96 unssd
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( A (,) B ) u. { B } ) C_ RR )
98 uncom
 |-  ( ( A (,) B ) u. { B } ) = ( { B } u. ( A (,) B ) )
99 98 difeq1i
 |-  ( ( ( A (,) B ) u. { B } ) \ ( A (,) B ) ) = ( ( { B } u. ( A (,) B ) ) \ ( A (,) B ) )
100 difun2
 |-  ( ( { B } u. ( A (,) B ) ) \ ( A (,) B ) ) = ( { B } \ ( A (,) B ) )
101 99 100 eqtri
 |-  ( ( ( A (,) B ) u. { B } ) \ ( A (,) B ) ) = ( { B } \ ( A (,) B ) )
102 difss
 |-  ( { B } \ ( A (,) B ) ) C_ { B }
103 101 102 eqsstri
 |-  ( ( ( A (,) B ) u. { B } ) \ ( A (,) B ) ) C_ { B }
104 ovolsn
 |-  ( B e. RR -> ( vol* ` { B } ) = 0 )
105 67 104 syl
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( vol* ` { B } ) = 0 )
106 ovolssnul
 |-  ( ( ( ( ( A (,) B ) u. { B } ) \ ( A (,) B ) ) C_ { B } /\ { B } C_ RR /\ ( vol* ` { B } ) = 0 ) -> ( vol* ` ( ( ( A (,) B ) u. { B } ) \ ( A (,) B ) ) ) = 0 )
107 103 96 105 106 mp3an2i
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( vol* ` ( ( ( A (,) B ) u. { B } ) \ ( A (,) B ) ) ) = 0 )
108 ssun1
 |-  ( ( A (,) B ) u. { B } ) C_ ( ( ( A (,) B ) u. { B } ) u. ( B (,) C ) )
109 108 88 sseqtrid
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( A (,) B ) u. { B } ) C_ ( A (,) C ) )
110 109 sselda
 |-  ( ( ( ph /\ ( A < B /\ B < C ) ) /\ x e. ( ( A (,) B ) u. { B } ) ) -> x e. ( A (,) C ) )
111 110 90 syldan
 |-  ( ( ( ph /\ ( A < B /\ B < C ) ) /\ x e. ( ( A (,) B ) u. { B } ) ) -> D e. CC )
112 93 97 107 111 itgss3
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( ( x e. ( A (,) B ) |-> D ) e. L^1 <-> ( x e. ( ( A (,) B ) u. { B } ) |-> D ) e. L^1 ) /\ S. ( A (,) B ) D _d x = S. ( ( A (,) B ) u. { B } ) D _d x ) )
113 112 simpld
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( ( x e. ( A (,) B ) |-> D ) e. L^1 <-> ( x e. ( ( A (,) B ) u. { B } ) |-> D ) e. L^1 ) )
114 91 113 mpbid
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( x e. ( ( A (,) B ) u. { B } ) |-> D ) e. L^1 )
115 6 adantr
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( x e. ( B (,) C ) |-> D ) e. L^1 )
116 85 89 90 114 115 itgsplit
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> S. ( A (,) C ) D _d x = ( S. ( ( A (,) B ) u. { B } ) D _d x + S. ( B (,) C ) D _d x ) )
117 112 simprd
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> S. ( A (,) B ) D _d x = S. ( ( A (,) B ) u. { B } ) D _d x )
118 117 oveq1d
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) = ( S. ( ( A (,) B ) u. { B } ) D _d x + S. ( B (,) C ) D _d x ) )
119 116 118 eqtr4d
 |-  ( ( ph /\ ( A < B /\ B < C ) ) -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) )
120 119 ex
 |-  ( ph -> ( ( A < B /\ B < C ) -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) ) )
121 36 60 120 ecased
 |-  ( ph -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) )