MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iblabs Unicode version

Theorem iblabs 19145
Description: The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
Hypotheses
Ref Expression
iblabs.1  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  V )
iblabs.2  |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )
Assertion
Ref Expression
iblabs  |-  ( ph  ->  ( x  e.  A  |->  ( abs `  B
) )  e.  L ^1 )
Distinct variable groups:    x, A    ph, x
Allowed substitution hints:    B( x)    V( x)

Proof of Theorem iblabs
StepHypRef Expression
1 iblabs.2 . . . . . 6  |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )
2 iblmbf 19084 . . . . . 6  |-  ( ( x  e.  A  |->  B )  e.  L ^1 
->  ( x  e.  A  |->  B )  e. MblFn )
31, 2syl 17 . . . . 5  |-  ( ph  ->  ( x  e.  A  |->  B )  e. MblFn )
4 iblabs.1 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  V )
53, 4mbfmptcl 18954 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  CC )
6 eqidd 2259 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B ) )
7 absf 11786 . . . . . 6  |-  abs : CC
--> RR
87a1i 12 . . . . 5  |-  ( ph  ->  abs : CC --> RR )
98feqmptd 5509 . . . 4  |-  ( ph  ->  abs  =  ( y  e.  CC  |->  ( abs `  y ) ) )
10 fveq2 5458 . . . 4  |-  ( y  =  B  ->  ( abs `  y )  =  ( abs `  B
) )
115, 6, 9, 10fmptco 5625 . . 3  |-  ( ph  ->  ( abs  o.  (
x  e.  A  |->  B ) )  =  ( x  e.  A  |->  ( abs `  B ) ) )
12 eqid 2258 . . . . 5  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
135, 12fmptd 5618 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  B ) : A --> CC )
14 ax-resscn 8762 . . . . . . 7  |-  RR  C_  CC
15 ssid 3172 . . . . . . 7  |-  CC  C_  CC
16 cncfss 18365 . . . . . . 7  |-  ( ( RR  C_  CC  /\  CC  C_  CC )  ->  ( CC -cn-> RR )  C_  ( CC -cn-> CC ) )
1714, 15, 16mp2an 656 . . . . . 6  |-  ( CC
-cn-> RR )  C_  ( CC -cn-> CC )
18 abscncf 18367 . . . . . 6  |-  abs  e.  ( CC -cn-> RR )
1917, 18sselii 3152 . . . . 5  |-  abs  e.  ( CC -cn-> CC )
2019a1i 12 . . . 4  |-  ( ph  ->  abs  e.  ( CC
-cn-> CC ) )
21 cncombf 18975 . . . 4  |-  ( ( ( x  e.  A  |->  B )  e. MblFn  /\  (
x  e.  A  |->  B ) : A --> CC  /\  abs  e.  ( CC -cn-> CC ) )  ->  ( abs  o.  ( x  e.  A  |->  B ) )  e. MblFn )
223, 13, 20, 21syl3anc 1187 . . 3  |-  ( ph  ->  ( abs  o.  (
x  e.  A  |->  B ) )  e. MblFn )
2311, 22eqeltrrd 2333 . 2  |-  ( ph  ->  ( x  e.  A  |->  ( abs `  B
) )  e. MblFn )
245abscld 11883 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  B )  e.  RR )
2524rexrd 8849 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  B )  e. 
RR* )
265absge0d 11891 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  0  <_  ( abs `  B
) )
27 elxrge0 10713 . . . . . . 7  |-  ( ( abs `  B )  e.  ( 0 [,] 
+oo )  <->  ( ( abs `  B )  e. 
RR*  /\  0  <_  ( abs `  B ) ) )
2825, 26, 27sylanbrc 648 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  B )  e.  ( 0 [,]  +oo ) )
29 0xr 8846 . . . . . . . 8  |-  0  e.  RR*
30 0le0 9795 . . . . . . . 8  |-  0  <_  0
31 elxrge0 10713 . . . . . . . 8  |-  ( 0  e.  ( 0 [,] 
+oo )  <->  ( 0  e.  RR*  /\  0  <_  0 ) )
3229, 30, 31mpbir2an 891 . . . . . . 7  |-  0  e.  ( 0 [,]  +oo )
3332a1i 12 . . . . . 6  |-  ( (
ph  /\  -.  x  e.  A )  ->  0  e.  ( 0 [,]  +oo ) )
3428, 33ifclda 3566 . . . . 5  |-  ( ph  ->  if ( x  e.  A ,  ( abs `  B ) ,  0 )  e.  ( 0 [,]  +oo ) )
3534adantr 453 . . . 4  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  A , 
( abs `  B
) ,  0 )  e.  ( 0 [,] 
+oo ) )
36 eqid 2258 . . . 4  |-  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  B
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  B
) ,  0 ) )
3735, 36fmptd 5618 . . 3  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
38 reex 8796 . . . . . . . . 9  |-  RR  e.  _V
3938a1i 12 . . . . . . . 8  |-  ( ph  ->  RR  e.  _V )
405recld 11644 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
Re `  B )  e.  RR )
4140recnd 8829 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
Re `  B )  e.  CC )
4241abscld 11883 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( Re `  B ) )  e.  RR )
4341absge0d 11891 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  0  <_  ( abs `  (
Re `  B )
) )
44 elrege0 10712 . . . . . . . . . . 11  |-  ( ( abs `  ( Re
`  B ) )  e.  ( 0 [,) 
+oo )  <->  ( ( abs `  ( Re `  B ) )  e.  RR  /\  0  <_ 
( abs `  (
Re `  B )
) ) )
4542, 43, 44sylanbrc 648 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( Re `  B ) )  e.  ( 0 [,)  +oo ) )
46 0re 8806 . . . . . . . . . . . 12  |-  0  e.  RR
47 elrege0 10712 . . . . . . . . . . . 12  |-  ( 0  e.  ( 0 [,) 
+oo )  <->  ( 0  e.  RR  /\  0  <_  0 ) )
4846, 30, 47mpbir2an 891 . . . . . . . . . . 11  |-  0  e.  ( 0 [,)  +oo )
4948a1i 12 . . . . . . . . . 10  |-  ( (
ph  /\  -.  x  e.  A )  ->  0  e.  ( 0 [,)  +oo ) )
5045, 49ifclda 3566 . . . . . . . . 9  |-  ( ph  ->  if ( x  e.  A ,  ( abs `  ( Re `  B
) ) ,  0 )  e.  ( 0 [,)  +oo ) )
5150adantr 453 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  A , 
( abs `  (
Re `  B )
) ,  0 )  e.  ( 0 [,) 
+oo ) )
525imcld 11645 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
Im `  B )  e.  RR )
5352recnd 8829 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
Im `  B )  e.  CC )
5453abscld 11883 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( Im `  B ) )  e.  RR )
5553absge0d 11891 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  0  <_  ( abs `  (
Im `  B )
) )
56 elrege0 10712 . . . . . . . . . . 11  |-  ( ( abs `  ( Im
`  B ) )  e.  ( 0 [,) 
+oo )  <->  ( ( abs `  ( Im `  B ) )  e.  RR  /\  0  <_ 
( abs `  (
Im `  B )
) ) )
5754, 55, 56sylanbrc 648 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( Im `  B ) )  e.  ( 0 [,)  +oo ) )
5857, 49ifclda 3566 . . . . . . . . 9  |-  ( ph  ->  if ( x  e.  A ,  ( abs `  ( Im `  B
) ) ,  0 )  e.  ( 0 [,)  +oo ) )
5958adantr 453 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 )  e.  ( 0 [,) 
+oo ) )
60 eqidd 2259 . . . . . . . 8  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Re `  B )
) ,  0 ) ) )
61 eqidd 2259 . . . . . . . 8  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 ) ) )
6239, 51, 59, 60, 61offval2 6029 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  ( Re
`  B ) ) ,  0 ) )  o F  +  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) ) )  =  ( x  e.  RR  |->  ( if ( x  e.  A ,  ( abs `  ( Re `  B
) ) ,  0 )  +  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 ) ) ) )
63 iftrue 3545 . . . . . . . . . . 11  |-  ( x  e.  A  ->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 )  =  ( abs `  (
Re `  B )
) )
64 iftrue 3545 . . . . . . . . . . 11  |-  ( x  e.  A  ->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 )  =  ( abs `  (
Im `  B )
) )
6563, 64oveq12d 5810 . . . . . . . . . 10  |-  ( x  e.  A  ->  ( if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 )  +  if ( x  e.  A ,  ( abs `  ( Im
`  B ) ) ,  0 ) )  =  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) )
66 iftrue 3545 . . . . . . . . . 10  |-  ( x  e.  A  ->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 )  =  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) )
6765, 66eqtr4d 2293 . . . . . . . . 9  |-  ( x  e.  A  ->  ( if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 )  +  if ( x  e.  A ,  ( abs `  ( Im
`  B ) ) ,  0 ) )  =  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) )
68 00id 8955 . . . . . . . . . 10  |-  ( 0  +  0 )  =  0
69 iffalse 3546 . . . . . . . . . . 11  |-  ( -.  x  e.  A  ->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 )  =  0 )
70 iffalse 3546 . . . . . . . . . . 11  |-  ( -.  x  e.  A  ->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 )  =  0 )
7169, 70oveq12d 5810 . . . . . . . . . 10  |-  ( -.  x  e.  A  -> 
( if ( x  e.  A ,  ( abs `  ( Re
`  B ) ) ,  0 )  +  if ( x  e.  A ,  ( abs `  ( Im `  B
) ) ,  0 ) )  =  ( 0  +  0 ) )
72 iffalse 3546 . . . . . . . . . 10  |-  ( -.  x  e.  A  ->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 )  =  0 )
7368, 71, 723eqtr4a 2316 . . . . . . . . 9  |-  ( -.  x  e.  A  -> 
( if ( x  e.  A ,  ( abs `  ( Re
`  B ) ) ,  0 )  +  if ( x  e.  A ,  ( abs `  ( Im `  B
) ) ,  0 ) )  =  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) )
7467, 73pm2.61i 158 . . . . . . . 8  |-  ( if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 )  +  if ( x  e.  A ,  ( abs `  ( Im
`  B ) ) ,  0 ) )  =  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 )
7574mpteq2i 4077 . . . . . . 7  |-  ( x  e.  RR  |->  ( if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 )  +  if ( x  e.  A ,  ( abs `  ( Im
`  B ) ) ,  0 ) ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) )
7662, 75syl6req 2307 . . . . . 6  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) )  =  ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) )  o F  +  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) ) ) )
7776fveq2d 5462 . . . . 5  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) )  =  ( S.2 `  ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) )  o F  +  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) ) ) ) )
78 eqid 2258 . . . . . . . 8  |-  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Re `  B )
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Re `  B )
) ,  0 ) )
795iblcn 19115 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  e.  A  |->  B )  e.  L ^1  <->  ( (
x  e.  A  |->  ( Re `  B ) )  e.  L ^1 
/\  ( x  e.  A  |->  ( Im `  B ) )  e.  L ^1 ) ) )
801, 79mpbid 203 . . . . . . . . 9  |-  ( ph  ->  ( ( x  e.  A  |->  ( Re `  B ) )  e.  L ^1  /\  (
x  e.  A  |->  ( Im `  B ) )  e.  L ^1 ) )
8180simpld 447 . . . . . . . 8  |-  ( ph  ->  ( x  e.  A  |->  ( Re `  B
) )  e.  L ^1 )
824, 1, 78, 81, 40iblabslem 19144 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  ( Re
`  B ) ) ,  0 ) )  e. MblFn  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) ) )  e.  RR ) )
8382simpld 447 . . . . . 6  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) )  e. MblFn )
8451, 78fmptd 5618 . . . . . 6  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) ) : RR --> ( 0 [,)  +oo ) )
8582simprd 451 . . . . . 6  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) ) )  e.  RR )
86 eqid 2258 . . . . . . . 8  |-  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 ) )
8780simprd 451 . . . . . . . 8  |-  ( ph  ->  ( x  e.  A  |->  ( Im `  B
) )  e.  L ^1 )
884, 1, 86, 87, 52iblabslem 19144 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  ( Im
`  B ) ) ,  0 ) )  e. MblFn  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) ) )  e.  RR ) )
8988simpld 447 . . . . . 6  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) )  e. MblFn )
9059, 86fmptd 5618 . . . . . 6  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) ) : RR --> ( 0 [,)  +oo ) )
9188simprd 451 . . . . . 6  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) ) )  e.  RR )
9283, 84, 85, 89, 90, 91itg2add 19076 . . . . 5  |-  ( ph  ->  ( S.2 `  (
( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) )  o F  +  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Im `  B )
) ,  0 ) ) ) )  =  ( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) ) )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 ) ) ) ) )
9377, 92eqtrd 2290 . . . 4  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) )  =  ( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) ) )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 ) ) ) ) )
9485, 91readdcld 8830 . . . 4  |-  ( ph  ->  ( ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  (
Re `  B )
) ,  0 ) ) )  +  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  (
Im `  B )
) ,  0 ) ) ) )  e.  RR )
9593, 94eqeltrd 2332 . . 3  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) )  e.  RR )
9642, 54readdcld 8830 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  (
( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) )  e.  RR )
9796rexrd 8849 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) )  e. 
RR* )
9842, 54, 43, 55addge0d 9316 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  0  <_  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) )
99 elxrge0 10713 . . . . . . . 8  |-  ( ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) )  e.  ( 0 [,]  +oo ) 
<->  ( ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) )  e.  RR*  /\  0  <_  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ) )
10097, 98, 99sylanbrc 648 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  (
( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) )  e.  ( 0 [,]  +oo ) )
101100, 33ifclda 3566 . . . . . 6  |-  ( ph  ->  if ( x  e.  A ,  ( ( abs `  ( Re
`  B ) )  +  ( abs `  (
Im `  B )
) ) ,  0 )  e.  ( 0 [,]  +oo ) )
102101adantr 453 . . . . 5  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  A , 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 )  e.  ( 0 [,]  +oo )
)
103 eqid 2258 . . . . 5  |-  ( x  e.  RR  |->  if ( x  e.  A , 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) )
104102, 103fmptd 5618 . . . 4  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) : RR --> ( 0 [,]  +oo ) )
105 ax-icn 8764 . . . . . . . . . . . 12  |-  _i  e.  CC
106 mulcl 8789 . . . . . . . . . . . 12  |-  ( ( _i  e.  CC  /\  ( Im `  B )  e.  CC )  -> 
( _i  x.  (
Im `  B )
)  e.  CC )
107105, 53, 106sylancr 647 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
_i  x.  ( Im `  B ) )  e.  CC )
10841, 107abstrid 11903 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( ( Re
`  B )  +  ( _i  x.  (
Im `  B )
) ) )  <_ 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( _i  x.  (
Im `  B )
) ) ) )
1095replimd 11647 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  B  =  ( ( Re
`  B )  +  ( _i  x.  (
Im `  B )
) ) )
110109fveq2d 5462 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  B )  =  ( abs `  (
( Re `  B
)  +  ( _i  x.  ( Im `  B ) ) ) ) )
111 absmul 11744 . . . . . . . . . . . . 13  |-  ( ( _i  e.  CC  /\  ( Im `  B )  e.  CC )  -> 
( abs `  (
_i  x.  ( Im `  B ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( Im `  B ) ) ) )
112105, 53, 111sylancr 647 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( _i  x.  ( Im `  B ) ) )  =  ( ( abs `  _i )  x.  ( abs `  ( Im `  B
) ) ) )
113 absi 11736 . . . . . . . . . . . . . 14  |-  ( abs `  _i )  =  1
114113oveq1i 5802 . . . . . . . . . . . . 13  |-  ( ( abs `  _i )  x.  ( abs `  (
Im `  B )
) )  =  ( 1  x.  ( abs `  ( Im `  B
) ) )
11554recnd 8829 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( Im `  B ) )  e.  CC )
116115mulid2d 8821 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
1  x.  ( abs `  ( Im `  B
) ) )  =  ( abs `  (
Im `  B )
) )
117114, 116syl5eq 2302 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( abs `  _i )  x.  ( abs `  ( Im `  B
) ) )  =  ( abs `  (
Im `  B )
) )
118112, 117eqtr2d 2291 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  ( Im `  B ) )  =  ( abs `  (
_i  x.  ( Im `  B ) ) ) )
119118oveq2d 5808 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) )  =  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( _i  x.  (
Im `  B )
) ) ) )
120108, 110, 1193brtr4d 4027 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( abs `  B )  <_ 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) )
121 iftrue 3545 . . . . . . . . . 10  |-  ( x  e.  A  ->  if ( x  e.  A ,  ( abs `  B
) ,  0 )  =  ( abs `  B
) )
122121adantl 454 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( x  e.  A ,  ( abs `  B
) ,  0 )  =  ( abs `  B
) )
12366adantl 454 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 )  =  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) )
124120, 122, 1233brtr4d 4027 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  if ( x  e.  A ,  ( abs `  B
) ,  0 )  <_  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) )
125124ex 425 . . . . . . 7  |-  ( ph  ->  ( x  e.  A  ->  if ( x  e.  A ,  ( abs `  B ) ,  0 )  <_  if (
x  e.  A , 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) ) )
12630a1i 12 . . . . . . . 8  |-  ( -.  x  e.  A  -> 
0  <_  0 )
127 iffalse 3546 . . . . . . . 8  |-  ( -.  x  e.  A  ->  if ( x  e.  A ,  ( abs `  B
) ,  0 )  =  0 )
128126, 127, 723brtr4d 4027 . . . . . . 7  |-  ( -.  x  e.  A  ->  if ( x  e.  A ,  ( abs `  B
) ,  0 )  <_  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) )
129125, 128pm2.61d1 153 . . . . . 6  |-  ( ph  ->  if ( x  e.  A ,  ( abs `  B ) ,  0 )  <_  if (
x  e.  A , 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) )
130129ralrimivw 2602 . . . . 5  |-  ( ph  ->  A. x  e.  RR  if ( x  e.  A ,  ( abs `  B
) ,  0 )  <_  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) )
131 eqidd 2259 . . . . . 6  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  B
) ,  0 ) ) )
132 eqidd 2259 . . . . . 6  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  A , 
( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) ) )
13339, 35, 102, 131, 132ofrfval2 6030 . . . . 5  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B ) ,  0 ) )  o R  <_  (
x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) )  <->  A. x  e.  RR  if ( x  e.  A ,  ( abs `  B
) ,  0 )  <_  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) ) )
134130, 133mpbird 225 . . . 4  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) )  o R  <_ 
( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) )
135 itg2le 19056 . . . 4  |-  ( ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  (
x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) )  o R  <_ 
( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) )  ->  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B ) ,  0 ) ) )  <_  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) ) )
13637, 104, 134, 135syl3anc 1187 . . 3  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) ) )  <_  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) ) ) )
137 itg2lecl 19055 . . 3  |-  ( ( ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) ) : RR --> ( 0 [,]  +oo )  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  (
Re `  B )
)  +  ( abs `  ( Im `  B
) ) ) ,  0 ) ) )  e.  RR  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B ) ,  0 ) ) )  <_  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( ( abs `  ( Re `  B
) )  +  ( abs `  ( Im
`  B ) ) ) ,  0 ) ) ) )  -> 
( S.2 `  ( x  e.  RR  |->  if ( x  e.  A , 
( abs `  B
) ,  0 ) ) )  e.  RR )
13837, 95, 136, 137syl3anc 1187 . 2  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B
) ,  0 ) ) )  e.  RR )
13924, 26iblpos 19109 . 2  |-  ( ph  ->  ( ( x  e.  A  |->  ( abs `  B
) )  e.  L ^1 
<->  ( ( x  e.  A  |->  ( abs `  B
) )  e. MblFn  /\  ( S.2 `  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  B ) ,  0 ) ) )  e.  RR ) ) )
14023, 138, 139mpbir2and 893 1  |-  ( ph  ->  ( x  e.  A  |->  ( abs `  B
) )  e.  L ^1 )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621   A.wral 2518   _Vcvv 2763    C_ wss 3127   ifcif 3539   class class class wbr 3997    e. cmpt 4051    o. ccom 4665   -->wf 4669   ` cfv 4673  (class class class)co 5792    o Fcof 6010    o Rcofr 6011   CCcc 8703   RRcr 8704   0cc0 8705   1c1 8706   _ici 8707    + caddc 8708    x. cmul 8710    +oocpnf 8832   RR*cxr 8834    <_ cle 8836   [,)cico 10624   [,]cicc 10625   Recre 11547   Imcim 11548   abscabs 11684   -cn->ccncf 18342  MblFncmbf 18931   S.2citg2 18933   L ^1cibl 18934
This theorem is referenced by:  iblmulc2  19147  itgabs  19151  bddmulibl  19155  itgcn  19159  ftc1a  19346  ftc1lem4  19348  itgulm  19746
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-rep 4105  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484  ax-inf2 7310  ax-cc 8029  ax-cnex 8761  ax-resscn 8762  ax-1cn 8763  ax-icn 8764  ax-addcl 8765  ax-addrcl 8766  ax-mulcl 8767  ax-mulrcl 8768  ax-mulcom 8769  ax-addass 8770  ax-mulass 8771  ax-distr 8772  ax-i2m1 8773  ax-1ne0 8774  ax-1rid 8775  ax-rnegex 8776  ax-rrecex 8777  ax-cnre 8778  ax-pre-lttri 8779  ax-pre-lttrn 8780  ax-pre-ltadd 8781  ax-pre-mulgt0 8782  ax-pre-sup 8783  ax-addf 8784  ax-mulf 8785
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-nel 2424  df-ral 2523  df-rex 2524  df-reu 2525  df-rmo 2526  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-pss 3143  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-tp 3622  df-op 3623  df-uni 3802  df-int 3837  df-iun 3881  df-iin 3882  df-disj 3968  df-br 3998  df-opab 4052  df-mpt 4053  df-tr 4088  df-eprel 4277  df-id 4281  df-po 4286  df-so 4287  df-fr 4324  df-se 4325  df-we 4326  df-ord 4367  df-on 4368  df-lim 4369  df-suc 4370  df-om 4629  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-fo 4687  df-f1o 4688  df-fv 4689  df-isom 4690  df-ov 5795  df-oprab 5796  df-mpt2 5797  df-of 6012  df-ofr 6013  df-1st 6056  df-2nd 6057  df-iota 6225  df-riota 6272  df-recs 6356  df-rdg 6391  df-1o 6447  df-2o 6448  df-oadd 6451  df-omul 6452  df-er 6628  df-map 6742  df-pm 6743  df-ixp 6786  df-en 6832  df-dom 6833  df-sdom 6834  df-fin 6835  df-fi 7133  df-sup 7162  df-oi 7193  df-card 7540  df-acn 7543  df-cda 7762  df-pnf 8837  df-mnf 8838  df-xr 8839  df-ltxr 8840  df-le 8841  df-sub 9007  df-neg 9008  df-div 9392  df-n 9715  df-2 9772  df-3 9773  df-4 9774  df-5 9775  df-6 9776  df-7 9777  df-8 9778  df-9 9779  df-10 9780  df-n0 9933  df-z 9992  df-dec 10092  df-uz 10198  df-q 10284  df-rp 10322  df-xneg 10419  df-xadd 10420  df-xmul 10421  df-ioo 10626  df-ioc 10627  df-ico 10628  df-icc 10629  df-fz 10749  df-fzo 10837  df-fl 10891  df-seq 11013  df-exp 11071  df-hash 11304  df-cj 11549  df-re 11550  df-im 11551  df-sqr 11685  df-abs 11686  df-clim 11927  df-rlim 11928  df-sum 12124  df-struct 13112  df-ndx 13113  df-slot 13114  df-base 13115  df-sets 13116  df-ress 13117  df-plusg 13183  df-mulr 13184  df-starv 13185  df-sca 13186  df-vsca 13187  df-tset 13189  df-ple 13190  df-ds 13192  df-hom 13194  df-cco 13195  df-rest 13289  df-topn 13290  df-topgen 13306  df-pt 13307  df-prds 13310  df-xrs 13365  df-0g 13366  df-gsum 13367  df-qtop 13372  df-imas 13373  df-xps 13375  df-mre 13450  df-mrc 13451  df-acs 13453  df-mnd 14329  df-submnd 14378  df-mulg 14454  df-cntz 14755  df-cmn 15053  df-xmet 16335  df-met 16336  df-bl 16337  df-mopn 16338  df-cnfld 16340  df-top 16598  df-bases 16600  df-topon 16601  df-topsp 16602  df-cn 16919  df-cnp 16920  df-cmp 17076  df-tx 17219  df-hmeo 17408  df-xms 17847  df-ms 17848  df-tms 17849  df-cncf 18344  df-ovol 18786  df-vol 18787  df-mbf 18937  df-itg1 18938  df-itg2 18939  df-ibl 18940  df-0p 18987
  Copyright terms: Public domain W3C validator