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

Metamath Proof Explorer

Theorem bddibl

Description: A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion bddibl 
|- ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> F e. L^1 )

Proof

Step Hyp Ref Expression
1 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
2 1 3ad2ant1 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> dom F e. dom vol )
3 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
4 3 3ad2ant1 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> F : dom F --> CC )
5 4 ffnd 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> F Fn dom F )
6 1cnd 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> 1 e. CC )
7 fnconstg 
 |-  ( 1 e. CC -> ( dom F X. { 1 } ) Fn dom F )
8 6 7 syl 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( dom F X. { 1 } ) Fn dom F )
9 eqidd 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) /\ z e. dom F ) -> ( F ` z ) = ( F ` z ) )
10 1ex 
 |-  1 e. _V
11 10 fvconst2 
 |-  ( z e. dom F -> ( ( dom F X. { 1 } ) ` z ) = 1 )
12 11 adantl 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) /\ z e. dom F ) -> ( ( dom F X. { 1 } ) ` z ) = 1 )
13 4 ffvelcdmda 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) /\ z e. dom F ) -> ( F ` z ) e. CC )
14 13 mulridd 
 |-  ( ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) /\ z e. dom F ) -> ( ( F ` z ) x. 1 ) = ( F ` z ) )
15 2 5 8 5 9 12 14 offveq 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( F oF x. ( dom F X. { 1 } ) ) = F )
16 simp2 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( vol ` dom F ) e. RR )
17 iblconst 
 |-  ( ( dom F e. dom vol /\ ( vol ` dom F ) e. RR /\ 1 e. CC ) -> ( dom F X. { 1 } ) e. L^1 )
18 2 16 6 17 syl3anc 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( dom F X. { 1 } ) e. L^1 )
19 bddmulibl 
 |-  ( ( F e. MblFn /\ ( dom F X. { 1 } ) e. L^1 /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( F oF x. ( dom F X. { 1 } ) ) e. L^1 )
20 18 19 syld3an2 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( F oF x. ( dom F X. { 1 } ) ) e. L^1 )
21 15 20 eqeltrrd 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> F e. L^1 )