Metamath Proof Explorer

Theorem iblre

Description: Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypothesis iblrelem.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion iblre 
|- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) ) )

Proof

Step Hyp Ref Expression
1 iblrelem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 1 mbfposb 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) ) )
3 ifan 
 |-  if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 )
4 3 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 ) )
5 4 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 ) ) )
6 5 eleq1i 
 |-  ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) e. RR )
7 ifan 
 |-  if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) = if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 )
8 7 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 ) )
9 8 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 ) ) )
10 9 eleq1i 
 |-  ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) e. RR )
11 6 10 anbi12i 
 |-  ( ( ( 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 ) <-> ( ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) e. RR ) )
12 11 a1i 
 |-  ( 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 /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR ) <-> ( ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) e. RR ) ) )
13 2 12 anbi12d 
 |-  ( 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 ) ) <-> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) /\ ( ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) e. RR ) ) ) )
14 3anass 
 |-  ( ( ( 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 ) ) )
15 an4 
 |-  ( ( ( ( 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 ) /\ ( ( 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 ) ) <-> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn ) /\ ( ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ B , B , 0 ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ -u B , -u B , 0 ) , 0 ) ) ) e. RR ) ) )
16 13 14 15 3bitr4g 
 |-  ( 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 ) <-> ( ( ( 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 ) /\ ( ( 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 ) ) ) )
17 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 ) ) )
18 0re 
 |-  0 e. RR
19 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
20 1 18 19 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
21 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
22 18 1 21 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
23 20 22 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 ) ) )
24 1 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
25 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
26 24 18 25 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
27 max1 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
28 18 24 27 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
29 26 28 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 ) ) )
30 23 29 anbi12d 
 |-  ( ph -> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u 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 ) /\ ( ( 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 ) ) ) )
31 16 17 30 3bitr4d 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) ) )