Step |
Hyp |
Ref |
Expression |
1 |
|
iccmbl |
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol ) |
2 |
|
cnmbf |
|- ( ( ( A [,] B ) e. dom vol /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. MblFn ) |
3 |
1 2
|
stoic3 |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. MblFn ) |
4 |
|
simp3 |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. ( ( A [,] B ) -cn-> CC ) ) |
5 |
|
cncff |
|- ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC ) |
6 |
|
fdm |
|- ( F : ( A [,] B ) --> CC -> dom F = ( A [,] B ) ) |
7 |
4 5 6
|
3syl |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> dom F = ( A [,] B ) ) |
8 |
7
|
fveq2d |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( vol ` dom F ) = ( vol ` ( A [,] B ) ) ) |
9 |
|
iccvolcl |
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,] B ) ) e. RR ) |
10 |
9
|
3adant3 |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( vol ` ( A [,] B ) ) e. RR ) |
11 |
8 10
|
eqeltrd |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( vol ` dom F ) e. RR ) |
12 |
|
cniccbdd |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) |
13 |
7
|
raleqdv |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( A. y e. dom F ( abs ` ( F ` y ) ) <_ x <-> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) ) |
14 |
13
|
rexbidv |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x <-> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) ) |
15 |
12 14
|
mpbird |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) |
16 |
|
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 ) |
17 |
3 11 15 16
|
syl3anc |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. L^1 ) |