Metamath Proof Explorer

Theorem itgreval

Description: Decompose the integral of a real function into positive and negative parts. (Contributed by Mario Carneiro, 31-Jul-2014)

Ref Expression
Hypotheses iblrelem.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
itgreval.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion itgreval 
|- ( ph -> S. A B _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) )

Proof

Step Hyp Ref Expression
1 iblrelem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 itgreval.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 1 2 itgrevallem1 
 |-  ( ph -> S. A B _d x = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) ) )
4 0re 
 |-  0 e. RR
5 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
6 1 4 5 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
7 1 iblrelem 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR ) ) )
8 2 7 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR ) )
9 8 simp1d 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
10 1 9 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
11 ifan 
 |-  if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 )
12 11 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) )
13 12 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) )
14 8 simp2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )
15 13 14 eqeltrrid 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) e. RR )
16 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
17 4 1 16 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
18 6 17 iblpos 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) e. RR ) ) )
19 10 15 18 mpbir2and 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 )
20 6 19 17 itgposval 
 |-  ( ph -> S. A if ( 0 <_ B , B , 0 ) _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) )
21 20 13 eqtr4di 
 |-  ( ph -> S. A if ( 0 <_ B , B , 0 ) _d x = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) )
22 1 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
23 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
24 22 4 23 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
25 1 9 mbfneg 
 |-  ( ph -> ( x e. A |-> -u B ) e. MblFn )
26 22 25 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )
27 ifan 
 |-  if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) = if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 )
28 27 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) = ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) )
29 28 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) )
30 8 simp3d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR )
31 29 30 eqeltrrid 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) e. RR )
32 max1 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
33 4 22 32 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
34 24 33 iblpos 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) e. RR ) ) )
35 26 31 34 mpbir2and 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 )
36 24 35 33 itgposval 
 |-  ( ph -> S. A if ( 0 <_ -u B , -u B , 0 ) _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) )
37 36 29 eqtr4di 
 |-  ( ph -> S. A if ( 0 <_ -u B , -u B , 0 ) _d x = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) )
38 21 37 oveq12d 
 |-  ( ph -> ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) ) )
39 3 38 eqtr4d 
 |-  ( ph -> S. A B _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) )