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 ) |