Metamath Proof Explorer

Theorem iblrelem

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

Ref Expression
Hypothesis iblrelem.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 iblrelem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
3 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
4 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
5 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
6 2 3 4 5 1 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) ) )
7 1 reim0d 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) = 0 )
8 7 itgvallem3 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) = 0 )
9 0re 
 |-  0 e. RR
10 8 9 eqeltrdi 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR )
11 7 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` B ) = -u 0 )
12 neg0 
 |-  -u 0 = 0
13 11 12 eqtrdi 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` B ) = 0 )
14 13 itgvallem3 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) = 0 )
15 14 9 eqeltrdi 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR )
16 10 15 jca 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) )
17 16 biantrud 
 |-  ( ph -> ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) <-> ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) ) )
18 1 rered 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) = B )
19 18 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ B ) , B , 0 ) )
20 19 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) )
21 20 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) )
22 21 eleq1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR ) )
23 18 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` B ) = -u B )
24 23 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) )
25 24 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) )
26 25 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) )
27 26 eleq1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR ) )
28 22 27 anbi12d 
 |-  ( ph -> ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) <-> ( ( 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 ) ) )
29 17 28 bitr3d 
 |-  ( ph -> ( ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) <-> ( ( 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 ) ) )
30 29 anbi2d 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. MblFn /\ ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` 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 ) ) ) )
31 3anass 
 |-  ( ( ( x e. A |-> B ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) <-> ( ( x e. A |-> B ) e. MblFn /\ ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) ) )
32 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 ) ) )
33 30 31 32 3bitr4g 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` 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 ) ) )
34 6 33 bitrd 
 |-  ( 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 ) ) )