Metamath Proof Explorer

Theorem ibl0

Description: The zero function is integrable on any measurable set. (Unlike iblconst , this does not require A to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion ibl0 
|- ( A e. dom vol -> ( A X. { 0 } ) e. L^1 )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 mbfconst 
 |-  ( ( A e. dom vol /\ 0 e. CC ) -> ( A X. { 0 } ) e. MblFn )
3 1 2 mpan2 
 |-  ( A e. dom vol -> ( A X. { 0 } ) e. MblFn )
4 ax-icn 
 |-  _i e. CC
5 ine0 
 |-  _i =/= 0
6 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
7 6 ad2antlr 
 |-  ( ( ( A e. dom vol /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> k e. ZZ )
8 expclz 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) e. CC )
9 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
10 8 9 div0d 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( 0 / ( _i ^ k ) ) = 0 )
11 4 5 7 10 mp3an12i 
 |-  ( ( ( A e. dom vol /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( 0 / ( _i ^ k ) ) = 0 )
12 11 fveq2d 
 |-  ( ( ( A e. dom vol /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( Re ` ( 0 / ( _i ^ k ) ) ) = ( Re ` 0 ) )
13 re0 
 |-  ( Re ` 0 ) = 0
14 12 13 eqtrdi 
 |-  ( ( ( A e. dom vol /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( Re ` ( 0 / ( _i ^ k ) ) ) = 0 )
15 14 itgvallem3 
 |-  ( ( A e. dom vol /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) ) = 0 )
16 0re 
 |-  0 e. RR
17 15 16 eqeltrdi 
 |-  ( ( A e. dom vol /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
18 17 ralrimiva 
 |-  ( A e. dom vol -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
19 eqidd 
 |-  ( A e. dom vol -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) )
20 eqidd 
 |-  ( ( A e. dom vol /\ x e. A ) -> ( Re ` ( 0 / ( _i ^ k ) ) ) = ( Re ` ( 0 / ( _i ^ k ) ) ) )
21 c0ex 
 |-  0 e. _V
22 21 fconst 
 |-  ( A X. { 0 } ) : A --> { 0 }
23 fdm 
 |-  ( ( A X. { 0 } ) : A --> { 0 } -> dom ( A X. { 0 } ) = A )
24 22 23 mp1i 
 |-  ( A e. dom vol -> dom ( A X. { 0 } ) = A )
25 21 fvconst2 
 |-  ( x e. A -> ( ( A X. { 0 } ) ` x ) = 0 )
26 25 adantl 
 |-  ( ( A e. dom vol /\ x e. A ) -> ( ( A X. { 0 } ) ` x ) = 0 )
27 19 20 24 26 isibl 
 |-  ( A e. dom vol -> ( ( A X. { 0 } ) e. L^1 <-> ( ( A X. { 0 } ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
28 3 18 27 mpbir2and 
 |-  ( A e. dom vol -> ( A X. { 0 } ) e. L^1 )