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

Metamath Proof Explorer

Theorem iblpos

Description: Integrability 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 )
iblpos.2 
|- ( ( ph /\ x e. A ) -> 0 <_ B )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 iblrelem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 iblpos.2 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
3 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 ) ) )
4 df-3an 
 |-  ( ( ( 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 ) <-> ( ( ( 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 ) )
5 3 4 bitrdi 
 |-  ( 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 ) ) )
6 1 2 iblposlem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = 0 )
7 0re 
 |-  0 e. RR
8 6 7 eqeltrdi 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR )
9 8 biantrud 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR ) <-> ( ( ( 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 ) ) )
10 2 ex 
 |-  ( ph -> ( x e. A -> 0 <_ B ) )
11 10 pm4.71rd 
 |-  ( ph -> ( x e. A <-> ( 0 <_ B /\ x e. A ) ) )
12 ancom 
 |-  ( ( 0 <_ B /\ x e. A ) <-> ( x e. A /\ 0 <_ B ) )
13 11 12 bitr2di 
 |-  ( ph -> ( ( x e. A /\ 0 <_ B ) <-> x e. A ) )
14 13 ifbid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , B , 0 ) )
15 14 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
16 15 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 ) ) ) )
17 16 eleq1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )
18 17 anbi2d 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR ) <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) ) )
19 5 9 18 3bitr2d 
 |-  ( 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 ) ) )