This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgposval

Description: The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

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

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 itgposval.3 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
4 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 ) ) ) ) )
5 3 ex 
 |-  ( ph -> ( x e. A -> 0 <_ B ) )
6 5 pm4.71rd 
 |-  ( ph -> ( x e. A <-> ( 0 <_ B /\ x e. A ) ) )
7 ancom 
 |-  ( ( 0 <_ B /\ x e. A ) <-> ( x e. A /\ 0 <_ B ) )
8 6 7 bitr2di 
 |-  ( ph -> ( ( x e. A /\ 0 <_ B ) <-> x e. A ) )
9 8 ifbid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , B , 0 ) )
10 9 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
11 10 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
12 1 3 iblposlem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = 0 )
13 11 12 oveq12d 
 |-  ( ph -> ( ( 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 ) ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) - 0 ) )
14 1 3 iblpos 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) ) )
15 2 14 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )
16 15 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR )
17 16 recnd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. CC )
18 17 subid1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) - 0 ) = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
19 4 13 18 3eqtrd 
 |-  ( ph -> S. A B _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )