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

Metamath Proof Explorer

Theorem bddmulibl

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

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

Proof

Step Hyp Ref Expression
1 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
2 1 ad2antrr 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> F : dom F --> CC )
3 2 ffnd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> F Fn dom F )
4 iblmbf 
 |-  ( G e. L^1 -> G e. MblFn )
5 4 ad2antlr 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> G e. MblFn )
6 mbff 
 |-  ( G e. MblFn -> G : dom G --> CC )
7 5 6 syl 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> G : dom G --> CC )
8 7 ffnd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> G Fn dom G )
9 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
10 9 ad2antrr 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> dom F e. dom vol )
11 mbfdm 
 |-  ( G e. MblFn -> dom G e. dom vol )
12 5 11 syl 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> dom G e. dom vol )
13 eqid 
 |-  ( dom F i^i dom G ) = ( dom F i^i dom G )
14 eqidd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. dom F ) -> ( F ` z ) = ( F ` z ) )
15 eqidd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. dom G ) -> ( G ` z ) = ( G ` z ) )
16 3 8 10 12 13 14 15 offval 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( F oF x. G ) = ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) )
17 ovexd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( ( F ` z ) x. ( G ` z ) ) e. _V )
18 simpll 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> F e. MblFn )
19 18 5 mbfmul 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( F oF x. G ) e. MblFn )
20 16 19 eqeltrrd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) e. MblFn )
21 absf 
 |-  abs : CC --> RR
22 21 a1i 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> abs : CC --> RR )
23 20 17 mbfmptcl 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( ( F ` z ) x. ( G ` z ) ) e. CC )
24 22 23 cofmpt 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( abs o. ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) ) = ( z e. ( dom F i^i dom G ) |-> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) ) )
25 23 fmpttd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) : ( dom F i^i dom G ) --> CC )
26 ax-resscn 
 |-  RR C_ CC
27 ssid 
 |-  CC C_ CC
28 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( CC -cn-> RR ) C_ ( CC -cn-> CC ) )
29 26 27 28 mp2an 
 |-  ( CC -cn-> RR ) C_ ( CC -cn-> CC )
30 abscncf 
 |-  abs e. ( CC -cn-> RR )
31 29 30 sselii 
 |-  abs e. ( CC -cn-> CC )
32 31 a1i 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> abs e. ( CC -cn-> CC ) )
33 cncombf 
 |-  ( ( ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) e. MblFn /\ ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) : ( dom F i^i dom G ) --> CC /\ abs e. ( CC -cn-> CC ) ) -> ( abs o. ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) ) e. MblFn )
34 20 25 32 33 syl3anc 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( abs o. ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) ) e. MblFn )
35 24 34 eqeltrrd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) |-> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) ) e. MblFn )
36 23 abscld 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) e. RR )
37 36 rexrd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) e. RR* )
38 23 absge0d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> 0 <_ ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) )
39 elxrge0 
 |-  ( ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) e. ( 0 [,] +oo ) <-> ( ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) e. RR* /\ 0 <_ ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) ) )
40 37 38 39 sylanbrc 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) e. ( 0 [,] +oo ) )
41 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
42 41 a1i 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. z e. ( dom F i^i dom G ) ) -> 0 e. ( 0 [,] +oo ) )
43 40 42 ifclda 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) e. ( 0 [,] +oo ) )
44 43 adantr 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. RR ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) e. ( 0 [,] +oo ) )
45 44 fmpttd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
46 reex 
 |-  RR e. _V
47 46 a1i 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> RR e. _V )
48 simprl 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> x e. RR )
49 48 ad2antrr 
 |-  ( ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) /\ z e. RR ) -> x e. RR )
50 elinel2 
 |-  ( z e. ( dom F i^i dom G ) -> z e. dom G )
51 ffvelcdm 
 |-  ( ( G : dom G --> CC /\ z e. dom G ) -> ( G ` z ) e. CC )
52 7 50 51 syl2an 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( G ` z ) e. CC )
53 52 abscld 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( G ` z ) ) e. RR )
54 52 absge0d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> 0 <_ ( abs ` ( G ` z ) ) )
55 elrege0 
 |-  ( ( abs ` ( G ` z ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( G ` z ) ) e. RR /\ 0 <_ ( abs ` ( G ` z ) ) ) )
56 53 54 55 sylanbrc 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( G ` z ) ) e. ( 0 [,) +oo ) )
57 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
58 57 a1i 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. z e. ( dom F i^i dom G ) ) -> 0 e. ( 0 [,) +oo ) )
59 56 58 ifclda 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) e. ( 0 [,) +oo ) )
60 59 ad2antrr 
 |-  ( ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) /\ z e. RR ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) e. ( 0 [,) +oo ) )
61 fconstmpt 
 |-  ( RR X. { x } ) = ( z e. RR |-> x )
62 61 a1i 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( RR X. { x } ) = ( z e. RR |-> x ) )
63 eqidd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) = ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) )
64 47 49 60 62 63 offval2 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( ( RR X. { x } ) oF x. ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) = ( z e. RR |-> ( x x. if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) )
65 ovif2 
 |-  ( x x. if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) = if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , ( x x. 0 ) )
66 48 recnd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> x e. CC )
67 66 adantr 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> x e. CC )
68 67 mul01d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( x x. 0 ) = 0 )
69 68 ifeq2d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , ( x x. 0 ) ) = if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) )
70 65 69 eqtrid 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( x x. if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) = if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) )
71 70 mpteq2dv 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( z e. RR |-> ( x x. if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) = ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) )
72 64 71 eqtrd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( ( RR X. { x } ) oF x. ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) = ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) )
73 72 fveq2d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( S.2 ` ( ( RR X. { x } ) oF x. ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) ) = ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) )
74 59 adantr 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. RR ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) e. ( 0 [,) +oo ) )
75 74 fmpttd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
76 75 adantr 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
77 inss2 
 |-  ( dom F i^i dom G ) C_ dom G
78 77 a1i 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( dom F i^i dom G ) C_ dom G )
79 20 17 mbfdm2 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( dom F i^i dom G ) e. dom vol )
80 7 ffvelcdmda 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. dom G ) -> ( G ` z ) e. CC )
81 7 feqmptd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> G = ( z e. dom G |-> ( G ` z ) ) )
82 simplr 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> G e. L^1 )
83 81 82 eqeltrrd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. dom G |-> ( G ` z ) ) e. L^1 )
84 78 79 80 83 iblss 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) |-> ( G ` z ) ) e. L^1 )
85 52 84 iblabs 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) |-> ( abs ` ( G ` z ) ) ) e. L^1 )
86 53 54 iblpos 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( ( z e. ( dom F i^i dom G ) |-> ( abs ` ( G ` z ) ) ) e. L^1 <-> ( ( z e. ( dom F i^i dom G ) |-> ( abs ` ( G ` z ) ) ) e. MblFn /\ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) e. RR ) ) )
87 85 86 mpbid 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( ( z e. ( dom F i^i dom G ) |-> ( abs ` ( G ` z ) ) ) e. MblFn /\ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) e. RR ) )
88 87 simprd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) e. RR )
89 88 adantr 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) e. RR )
90 simplrl 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> x e. RR )
91 neq0 
 |-  ( -. ( dom F i^i dom G ) = (/) <-> E. z z e. ( dom F i^i dom G ) )
92 0re 
 |-  0 e. RR
93 92 a1i 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> 0 e. RR )
94 elinel1 
 |-  ( z e. ( dom F i^i dom G ) -> z e. dom F )
95 ffvelcdm 
 |-  ( ( F : dom F --> CC /\ z e. dom F ) -> ( F ` z ) e. CC )
96 2 94 95 syl2an 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( F ` z ) e. CC )
97 96 abscld 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( F ` z ) ) e. RR )
98 simplrl 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> x e. RR )
99 96 absge0d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> 0 <_ ( abs ` ( F ` z ) ) )
100 simprr 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
101 2fveq3 
 |-  ( y = z -> ( abs ` ( F ` y ) ) = ( abs ` ( F ` z ) ) )
102 101 breq1d 
 |-  ( y = z -> ( ( abs ` ( F ` y ) ) <_ x <-> ( abs ` ( F ` z ) ) <_ x ) )
103 102 rspccva 
 |-  ( ( A. y e. dom F ( abs ` ( F ` y ) ) <_ x /\ z e. dom F ) -> ( abs ` ( F ` z ) ) <_ x )
104 100 94 103 syl2an 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( F ` z ) ) <_ x )
105 93 97 98 99 104 letrd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> 0 <_ x )
106 105 ex 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) -> 0 <_ x ) )
107 106 exlimdv 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( E. z z e. ( dom F i^i dom G ) -> 0 <_ x ) )
108 91 107 biimtrid 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( -. ( dom F i^i dom G ) = (/) -> 0 <_ x ) )
109 108 imp 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> 0 <_ x )
110 elrege0 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
111 90 109 110 sylanbrc 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> x e. ( 0 [,) +oo ) )
112 76 89 111 itg2mulc 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( S.2 ` ( ( RR X. { x } ) oF x. ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) ) = ( x x. ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) ) )
113 73 112 eqtr3d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) = ( x x. ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) ) )
114 90 89 remulcld 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( x x. ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( G ` z ) ) , 0 ) ) ) ) e. RR )
115 113 114 eqeltrd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. ( dom F i^i dom G ) = (/) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) e. RR )
116 115 ex 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( -. ( dom F i^i dom G ) = (/) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) e. RR ) )
117 noel 
 |-  -. z e. (/)
118 eleq2 
 |-  ( ( dom F i^i dom G ) = (/) -> ( z e. ( dom F i^i dom G ) <-> z e. (/) ) )
119 117 118 mtbiri 
 |-  ( ( dom F i^i dom G ) = (/) -> -. z e. ( dom F i^i dom G ) )
120 iffalse 
 |-  ( -. z e. ( dom F i^i dom G ) -> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) = 0 )
121 119 120 syl 
 |-  ( ( dom F i^i dom G ) = (/) -> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) = 0 )
122 121 mpteq2dv 
 |-  ( ( dom F i^i dom G ) = (/) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) = ( z e. RR |-> 0 ) )
123 fconstmpt 
 |-  ( RR X. { 0 } ) = ( z e. RR |-> 0 )
124 122 123 eqtr4di 
 |-  ( ( dom F i^i dom G ) = (/) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) = ( RR X. { 0 } ) )
125 124 fveq2d 
 |-  ( ( dom F i^i dom G ) = (/) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) = ( S.2 ` ( RR X. { 0 } ) ) )
126 itg20 
 |-  ( S.2 ` ( RR X. { 0 } ) ) = 0
127 126 92 eqeltri 
 |-  ( S.2 ` ( RR X. { 0 } ) ) e. RR
128 125 127 eqeltrdi 
 |-  ( ( dom F i^i dom G ) = (/) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) e. RR )
129 116 128 pm2.61d2 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) e. RR )
130 98 53 remulcld 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( x x. ( abs ` ( G ` z ) ) ) e. RR )
131 130 rexrd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( x x. ( abs ` ( G ` z ) ) ) e. RR* )
132 98 53 105 54 mulge0d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> 0 <_ ( x x. ( abs ` ( G ` z ) ) ) )
133 elxrge0 
 |-  ( ( x x. ( abs ` ( G ` z ) ) ) e. ( 0 [,] +oo ) <-> ( ( x x. ( abs ` ( G ` z ) ) ) e. RR* /\ 0 <_ ( x x. ( abs ` ( G ` z ) ) ) ) )
134 131 132 133 sylanbrc 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( x x. ( abs ` ( G ` z ) ) ) e. ( 0 [,] +oo ) )
135 134 42 ifclda 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) e. ( 0 [,] +oo ) )
136 135 adantr 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. RR ) -> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) e. ( 0 [,] +oo ) )
137 136 fmpttd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
138 96 52 absmuld 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) = ( ( abs ` ( F ` z ) ) x. ( abs ` ( G ` z ) ) ) )
139 abscl 
 |-  ( ( G ` z ) e. CC -> ( abs ` ( G ` z ) ) e. RR )
140 absge0 
 |-  ( ( G ` z ) e. CC -> 0 <_ ( abs ` ( G ` z ) ) )
141 139 140 jca 
 |-  ( ( G ` z ) e. CC -> ( ( abs ` ( G ` z ) ) e. RR /\ 0 <_ ( abs ` ( G ` z ) ) ) )
142 52 141 syl 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( ( abs ` ( G ` z ) ) e. RR /\ 0 <_ ( abs ` ( G ` z ) ) ) )
143 lemul1a 
 |-  ( ( ( ( abs ` ( F ` z ) ) e. RR /\ x e. RR /\ ( ( abs ` ( G ` z ) ) e. RR /\ 0 <_ ( abs ` ( G ` z ) ) ) ) /\ ( abs ` ( F ` z ) ) <_ x ) -> ( ( abs ` ( F ` z ) ) x. ( abs ` ( G ` z ) ) ) <_ ( x x. ( abs ` ( G ` z ) ) ) )
144 97 98 142 104 143 syl31anc 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( ( abs ` ( F ` z ) ) x. ( abs ` ( G ` z ) ) ) <_ ( x x. ( abs ` ( G ` z ) ) ) )
145 138 144 eqbrtrd 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) <_ ( x x. ( abs ` ( G ` z ) ) ) )
146 iftrue 
 |-  ( z e. ( dom F i^i dom G ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) = ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) )
147 146 adantl 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) = ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) )
148 iftrue 
 |-  ( z e. ( dom F i^i dom G ) -> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) = ( x x. ( abs ` ( G ` z ) ) ) )
149 148 adantl 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) = ( x x. ( abs ` ( G ` z ) ) ) )
150 145 147 149 3brtr4d 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ z e. ( dom F i^i dom G ) ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) <_ if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) )
151 0le0 
 |-  0 <_ 0
152 151 a1i 
 |-  ( -. z e. ( dom F i^i dom G ) -> 0 <_ 0 )
153 iffalse 
 |-  ( -. z e. ( dom F i^i dom G ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) = 0 )
154 152 153 120 3brtr4d 
 |-  ( -. z e. ( dom F i^i dom G ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) <_ if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) )
155 154 adantl 
 |-  ( ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) /\ -. z e. ( dom F i^i dom G ) ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) <_ if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) )
156 150 155 pm2.61dan 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) <_ if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) )
157 156 ralrimivw 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> A. z e. RR if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) <_ if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) )
158 46 a1i 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> RR e. _V )
159 eqidd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) = ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) )
160 eqidd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) = ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) )
161 158 44 136 159 160 ofrfval2 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) oR <_ ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) <-> A. z e. RR if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) <_ if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) )
162 157 161 mpbird 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) oR <_ ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) )
163 itg2le 
 |-  ( ( ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) oR <_ ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) ) <_ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) )
164 45 137 162 163 syl3anc 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) ) <_ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) )
165 itg2lecl 
 |-  ( ( ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) ) <_ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( x x. ( abs ` ( G ` z ) ) ) , 0 ) ) ) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) ) e. RR )
166 45 129 164 165 syl3anc 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) ) e. RR )
167 36 38 iblpos 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( ( z e. ( dom F i^i dom G ) |-> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) ) e. L^1 <-> ( ( z e. ( dom F i^i dom G ) |-> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) ) e. MblFn /\ ( S.2 ` ( z e. RR |-> if ( z e. ( dom F i^i dom G ) , ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) , 0 ) ) ) e. RR ) ) )
168 35 166 167 mpbir2and 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) |-> ( abs ` ( ( F ` z ) x. ( G ` z ) ) ) ) e. L^1 )
169 17 20 168 iblabsr 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( z e. ( dom F i^i dom G ) |-> ( ( F ` z ) x. ( G ` z ) ) ) e. L^1 )
170 16 169 eqeltrd 
 |-  ( ( ( F e. MblFn /\ G e. L^1 ) /\ ( x e. RR /\ A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) ) -> ( F oF x. G ) e. L^1 )
171 170 rexlimdvaa 
 |-  ( ( F e. MblFn /\ G e. L^1 ) -> ( E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x -> ( F oF x. G ) e. L^1 ) )
172 171 3impia 
 |-  ( ( F e. MblFn /\ G e. L^1 /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( F oF x. G ) e. L^1 )