Metamath Proof Explorer

Theorem ditgsplitlem

Description: Lemma for ditgsplit . (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses ditgsplit.x 
|- ( ph -> X e. RR )
ditgsplit.y 
|- ( ph -> Y e. RR )
ditgsplit.a 
|- ( ph -> A e. ( X [,] Y ) )
ditgsplit.b 
|- ( ph -> B e. ( X [,] Y ) )
ditgsplit.c 
|- ( ph -> C e. ( X [,] Y ) )
ditgsplit.d 
|- ( ( ph /\ x e. ( X (,) Y ) ) -> D e. V )
ditgsplit.i 
|- ( ph -> ( x e. ( X (,) Y ) |-> D ) e. L^1 )
ditgsplit.1 
|- ( ( ps /\ th ) <-> ( A <_ B /\ B <_ C ) )
Assertion ditgsplitlem 
|- ( ( ( ph /\ ps ) /\ th ) -> S_ [ A -> C ] D _d x = ( S_ [ A -> B ] D _d x + S_ [ B -> C ] D _d x ) )

Proof

Step Hyp Ref Expression
1 ditgsplit.x 
 |-  ( ph -> X e. RR )
2 ditgsplit.y 
 |-  ( ph -> Y e. RR )
3 ditgsplit.a 
 |-  ( ph -> A e. ( X [,] Y ) )
4 ditgsplit.b 
 |-  ( ph -> B e. ( X [,] Y ) )
5 ditgsplit.c 
 |-  ( ph -> C e. ( X [,] Y ) )
6 ditgsplit.d 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> D e. V )
7 ditgsplit.i 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> D ) e. L^1 )
8 ditgsplit.1 
 |-  ( ( ps /\ th ) <-> ( A <_ B /\ B <_ C ) )
9 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( A e. ( X [,] Y ) <-> ( A e. RR /\ X <_ A /\ A <_ Y ) ) )
10 1 2 9 syl2anc 
 |-  ( ph -> ( A e. ( X [,] Y ) <-> ( A e. RR /\ X <_ A /\ A <_ Y ) ) )
11 3 10 mpbid 
 |-  ( ph -> ( A e. RR /\ X <_ A /\ A <_ Y ) )
12 11 simp1d 
 |-  ( ph -> A e. RR )
13 12 adantr 
 |-  ( ( ph /\ ( ps /\ th ) ) -> A e. RR )
14 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( C e. ( X [,] Y ) <-> ( C e. RR /\ X <_ C /\ C <_ Y ) ) )
15 1 2 14 syl2anc 
 |-  ( ph -> ( C e. ( X [,] Y ) <-> ( C e. RR /\ X <_ C /\ C <_ Y ) ) )
16 5 15 mpbid 
 |-  ( ph -> ( C e. RR /\ X <_ C /\ C <_ Y ) )
17 16 simp1d 
 |-  ( ph -> C e. RR )
18 17 adantr 
 |-  ( ( ph /\ ( ps /\ th ) ) -> C e. RR )
19 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( B e. ( X [,] Y ) <-> ( B e. RR /\ X <_ B /\ B <_ Y ) ) )
20 1 2 19 syl2anc 
 |-  ( ph -> ( B e. ( X [,] Y ) <-> ( B e. RR /\ X <_ B /\ B <_ Y ) ) )
21 4 20 mpbid 
 |-  ( ph -> ( B e. RR /\ X <_ B /\ B <_ Y ) )
22 21 simp1d 
 |-  ( ph -> B e. RR )
23 22 adantr 
 |-  ( ( ph /\ ( ps /\ th ) ) -> B e. RR )
24 8 bilani 
 |-  ( ( ph /\ ( ps /\ th ) ) -> ( A <_ B /\ B <_ C ) )
25 24 simpld 
 |-  ( ( ph /\ ( ps /\ th ) ) -> A <_ B )
26 24 simprd 
 |-  ( ( ph /\ ( ps /\ th ) ) -> B <_ C )
27 elicc2 
 |-  ( ( A e. RR /\ C e. RR ) -> ( B e. ( A [,] C ) <-> ( B e. RR /\ A <_ B /\ B <_ C ) ) )
28 12 17 27 syl2anc 
 |-  ( ph -> ( B e. ( A [,] C ) <-> ( B e. RR /\ A <_ B /\ B <_ C ) ) )
29 28 adantr 
 |-  ( ( ph /\ ( ps /\ th ) ) -> ( B e. ( A [,] C ) <-> ( B e. RR /\ A <_ B /\ B <_ C ) ) )
30 23 25 26 29 mpbir3and 
 |-  ( ( ph /\ ( ps /\ th ) ) -> B e. ( A [,] C ) )
31 1 rexrd 
 |-  ( ph -> X e. RR* )
32 11 simp2d 
 |-  ( ph -> X <_ A )
33 iooss1 
 |-  ( ( X e. RR* /\ X <_ A ) -> ( A (,) C ) C_ ( X (,) C ) )
34 31 32 33 syl2anc 
 |-  ( ph -> ( A (,) C ) C_ ( X (,) C ) )
35 2 rexrd 
 |-  ( ph -> Y e. RR* )
36 16 simp3d 
 |-  ( ph -> C <_ Y )
37 iooss2 
 |-  ( ( Y e. RR* /\ C <_ Y ) -> ( X (,) C ) C_ ( X (,) Y ) )
38 35 36 37 syl2anc 
 |-  ( ph -> ( X (,) C ) C_ ( X (,) Y ) )
39 34 38 sstrd 
 |-  ( ph -> ( A (,) C ) C_ ( X (,) Y ) )
40 39 sselda 
 |-  ( ( ph /\ x e. ( A (,) C ) ) -> x e. ( X (,) Y ) )
41 iblmbf 
 |-  ( ( x e. ( X (,) Y ) |-> D ) e. L^1 -> ( x e. ( X (,) Y ) |-> D ) e. MblFn )
42 7 41 syl 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> D ) e. MblFn )
43 42 6 mbfmptcl 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> D e. CC )
44 40 43 syldan 
 |-  ( ( ph /\ x e. ( A (,) C ) ) -> D e. CC )
45 44 adantlr 
 |-  ( ( ( ph /\ ( ps /\ th ) ) /\ x e. ( A (,) C ) ) -> D e. CC )
46 iooss1 
 |-  ( ( X e. RR* /\ X <_ A ) -> ( A (,) B ) C_ ( X (,) B ) )
47 31 32 46 syl2anc 
 |-  ( ph -> ( A (,) B ) C_ ( X (,) B ) )
48 21 simp3d 
 |-  ( ph -> B <_ Y )
49 iooss2 
 |-  ( ( Y e. RR* /\ B <_ Y ) -> ( X (,) B ) C_ ( X (,) Y ) )
50 35 48 49 syl2anc 
 |-  ( ph -> ( X (,) B ) C_ ( X (,) Y ) )
51 47 50 sstrd 
 |-  ( ph -> ( A (,) B ) C_ ( X (,) Y ) )
52 ioombl 
 |-  ( A (,) B ) e. dom vol
53 52 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
54 51 53 6 7 iblss 
 |-  ( ph -> ( x e. ( A (,) B ) |-> D ) e. L^1 )
55 54 adantr 
 |-  ( ( ph /\ ( ps /\ th ) ) -> ( x e. ( A (,) B ) |-> D ) e. L^1 )
56 21 simp2d 
 |-  ( ph -> X <_ B )
57 iooss1 
 |-  ( ( X e. RR* /\ X <_ B ) -> ( B (,) C ) C_ ( X (,) C ) )
58 31 56 57 syl2anc 
 |-  ( ph -> ( B (,) C ) C_ ( X (,) C ) )
59 58 38 sstrd 
 |-  ( ph -> ( B (,) C ) C_ ( X (,) Y ) )
60 ioombl 
 |-  ( B (,) C ) e. dom vol
61 60 a1i 
 |-  ( ph -> ( B (,) C ) e. dom vol )
62 59 61 6 7 iblss 
 |-  ( ph -> ( x e. ( B (,) C ) |-> D ) e. L^1 )
63 62 adantr 
 |-  ( ( ph /\ ( ps /\ th ) ) -> ( x e. ( B (,) C ) |-> D ) e. L^1 )
64 13 18 30 45 55 63 itgsplitioo 
 |-  ( ( ph /\ ( ps /\ th ) ) -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) )
65 13 23 18 25 26 letrd 
 |-  ( ( ph /\ ( ps /\ th ) ) -> A <_ C )
66 65 ditgpos 
 |-  ( ( ph /\ ( ps /\ th ) ) -> S_ [ A -> C ] D _d x = S. ( A (,) C ) D _d x )
67 25 ditgpos 
 |-  ( ( ph /\ ( ps /\ th ) ) -> S_ [ A -> B ] D _d x = S. ( A (,) B ) D _d x )
68 26 ditgpos 
 |-  ( ( ph /\ ( ps /\ th ) ) -> S_ [ B -> C ] D _d x = S. ( B (,) C ) D _d x )
69 67 68 oveq12d 
 |-  ( ( ph /\ ( ps /\ th ) ) -> ( S_ [ A -> B ] D _d x + S_ [ B -> C ] D _d x ) = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) )
70 64 66 69 3eqtr4d 
 |-  ( ( ph /\ ( ps /\ th ) ) -> S_ [ A -> C ] D _d x = ( S_ [ A -> B ] D _d x + S_ [ B -> C ] D _d x ) )
71 70 anassrs 
 |-  ( ( ( ph /\ ps ) /\ th ) -> S_ [ A -> C ] D _d x = ( S_ [ A -> B ] D _d x + S_ [ B -> C ] D _d x ) )