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