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 eqtrid 
 |-  ( ( 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 eqtrid 
 |-  ( ( 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 ) )