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 ffvelrnda
 |-  ( ( ( 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 mulid1d
 |-  ( ( ( 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 )