Metamath Proof Explorer

Theorem itgspliticc

Description: The S. integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses itgspliticc.1 
|- ( ph -> A e. RR )
itgspliticc.2 
|- ( ph -> C e. RR )
itgspliticc.3 
|- ( ph -> B e. ( A [,] C ) )
itgspliticc.4 
|- ( ( ph /\ x e. ( A [,] C ) ) -> D e. V )
itgspliticc.5 
|- ( ph -> ( x e. ( A [,] B ) |-> D ) e. L^1 )
itgspliticc.6 
|- ( ph -> ( x e. ( B [,] C ) |-> D ) e. L^1 )
Assertion itgspliticc 
|- ( 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 itgspliticc.1 
 |-  ( ph -> A e. RR )
2 itgspliticc.2 
 |-  ( ph -> C e. RR )
3 itgspliticc.3 
 |-  ( ph -> B e. ( A [,] C ) )
4 itgspliticc.4 
 |-  ( ( ph /\ x e. ( A [,] C ) ) -> D e. V )
5 itgspliticc.5 
 |-  ( ph -> ( x e. ( A [,] B ) |-> D ) e. L^1 )
6 itgspliticc.6 
 |-  ( ph -> ( x e. ( B [,] C ) |-> D ) e. L^1 )
7 1 rexrd 
 |-  ( ph -> A e. RR* )
8 elicc2 
 |-  ( ( A e. RR /\ C e. RR ) -> ( B e. ( A [,] C ) <-> ( B e. RR /\ A <_ B /\ B <_ C ) ) )
9 1 2 8 syl2anc 
 |-  ( ph -> ( B e. ( A [,] C ) <-> ( B e. RR /\ A <_ B /\ B <_ C ) ) )
10 3 9 mpbid 
 |-  ( ph -> ( B e. RR /\ A <_ B /\ B <_ C ) )
11 10 simp1d 
 |-  ( ph -> B e. RR )
12 11 rexrd 
 |-  ( ph -> B e. RR* )
13 2 rexrd 
 |-  ( ph -> C e. RR* )
14 df-icc 
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
15 xrmaxle 
 |-  ( ( A e. RR* /\ B e. RR* /\ z e. RR* ) -> ( if ( A <_ B , B , A ) <_ z <-> ( A <_ z /\ B <_ z ) ) )
16 xrlemin 
 |-  ( ( z e. RR* /\ B e. RR* /\ C e. RR* ) -> ( z <_ if ( B <_ C , B , C ) <-> ( z <_ B /\ z <_ C ) ) )
17 14 15 16 ixxin 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( B e. RR* /\ C e. RR* ) ) -> ( ( A [,] B ) i^i ( B [,] C ) ) = ( if ( A <_ B , B , A ) [,] if ( B <_ C , B , C ) ) )
18 7 12 12 13 17 syl22anc 
 |-  ( ph -> ( ( A [,] B ) i^i ( B [,] C ) ) = ( if ( A <_ B , B , A ) [,] if ( B <_ C , B , C ) ) )
19 10 simp2d 
 |-  ( ph -> A <_ B )
20 19 iftrued 
 |-  ( ph -> if ( A <_ B , B , A ) = B )
21 10 simp3d 
 |-  ( ph -> B <_ C )
22 21 iftrued 
 |-  ( ph -> if ( B <_ C , B , C ) = B )
23 20 22 oveq12d 
 |-  ( ph -> ( if ( A <_ B , B , A ) [,] if ( B <_ C , B , C ) ) = ( B [,] B ) )
24 iccid 
 |-  ( B e. RR* -> ( B [,] B ) = { B } )
25 12 24 syl 
 |-  ( ph -> ( B [,] B ) = { B } )
26 18 23 25 3eqtrd 
 |-  ( ph -> ( ( A [,] B ) i^i ( B [,] C ) ) = { B } )
27 26 fveq2d 
 |-  ( ph -> ( vol* ` ( ( A [,] B ) i^i ( B [,] C ) ) ) = ( vol* ` { B } ) )
28 ovolsn 
 |-  ( B e. RR -> ( vol* ` { B } ) = 0 )
29 11 28 syl 
 |-  ( ph -> ( vol* ` { B } ) = 0 )
30 27 29 eqtrd 
 |-  ( ph -> ( vol* ` ( ( A [,] B ) i^i ( B [,] C ) ) ) = 0 )
31 iccsplit 
 |-  ( ( A e. RR /\ C e. RR /\ B e. ( A [,] C ) ) -> ( A [,] C ) = ( ( A [,] B ) u. ( B [,] C ) ) )
32 1 2 3 31 syl3anc 
 |-  ( ph -> ( A [,] C ) = ( ( A [,] B ) u. ( B [,] C ) ) )
33 30 32 4 5 6 itgsplit 
 |-  ( ph -> S. ( A [,] C ) D _d x = ( S. ( A [,] B ) D _d x + S. ( B [,] C ) D _d x ) )