Metamath Proof Explorer


Theorem iblabs

Description: The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses iblabs.1
|- ( ( ph /\ x e. A ) -> B e. V )
iblabs.2
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion iblabs
|- ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )

Proof

Step Hyp Ref Expression
1 iblabs.1
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 iblabs.2
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 absf
 |-  abs : CC --> RR
4 3 a1i
 |-  ( ph -> abs : CC --> RR )
5 iblmbf
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
6 2 5 syl
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
7 6 1 mbfmptcl
 |-  ( ( ph /\ x e. A ) -> B e. CC )
8 4 7 cofmpt
 |-  ( ph -> ( abs o. ( x e. A |-> B ) ) = ( x e. A |-> ( abs ` B ) ) )
9 7 fmpttd
 |-  ( ph -> ( x e. A |-> B ) : A --> CC )
10 ax-resscn
 |-  RR C_ CC
11 ssid
 |-  CC C_ CC
12 cncfss
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( CC -cn-> RR ) C_ ( CC -cn-> CC ) )
13 10 11 12 mp2an
 |-  ( CC -cn-> RR ) C_ ( CC -cn-> CC )
14 abscncf
 |-  abs e. ( CC -cn-> RR )
15 13 14 sselii
 |-  abs e. ( CC -cn-> CC )
16 15 a1i
 |-  ( ph -> abs e. ( CC -cn-> CC ) )
17 cncombf
 |-  ( ( ( 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 )
18 6 9 16 17 syl3anc
 |-  ( ph -> ( abs o. ( x e. A |-> B ) ) e. MblFn )
19 8 18 eqeltrrd
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. MblFn )
20 7 abscld
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
21 20 rexrd
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR* )
22 7 absge0d
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( abs ` B ) )
23 elxrge0
 |-  ( ( abs ` B ) e. ( 0 [,] +oo ) <-> ( ( abs ` B ) e. RR* /\ 0 <_ ( abs ` B ) ) )
24 21 22 23 sylanbrc
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. ( 0 [,] +oo ) )
25 0e0iccpnf
 |-  0 e. ( 0 [,] +oo )
26 25 a1i
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
27 24 26 ifclda
 |-  ( ph -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,] +oo ) )
28 27 adantr
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,] +oo ) )
29 28 fmpttd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
30 reex
 |-  RR e. _V
31 30 a1i
 |-  ( ph -> RR e. _V )
32 7 recld
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
33 32 recnd
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
34 33 abscld
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( Re ` B ) ) e. RR )
35 33 absge0d
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( abs ` ( Re ` B ) ) )
36 elrege0
 |-  ( ( abs ` ( Re ` B ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( Re ` B ) ) e. RR /\ 0 <_ ( abs ` ( Re ` B ) ) ) )
37 34 35 36 sylanbrc
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( Re ` B ) ) e. ( 0 [,) +oo ) )
38 0e0icopnf
 |-  0 e. ( 0 [,) +oo )
39 38 a1i
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
40 37 39 ifclda
 |-  ( ph -> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) e. ( 0 [,) +oo ) )
41 40 adantr
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) e. ( 0 [,) +oo ) )
42 7 imcld
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
43 42 recnd
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
44 43 abscld
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( Im ` B ) ) e. RR )
45 43 absge0d
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( abs ` ( Im ` B ) ) )
46 elrege0
 |-  ( ( abs ` ( Im ` B ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( Im ` B ) ) e. RR /\ 0 <_ ( abs ` ( Im ` B ) ) ) )
47 44 45 46 sylanbrc
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( Im ` B ) ) e. ( 0 [,) +oo ) )
48 47 39 ifclda
 |-  ( ph -> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) e. ( 0 [,) +oo ) )
49 48 adantr
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) e. ( 0 [,) +oo ) )
50 eqidd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) )
51 eqidd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) )
52 31 41 49 50 51 offval2
 |-  ( ph -> ( ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) oF + ( 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 ) ) ) )
53 iftrue
 |-  ( x e. A -> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) = ( abs ` ( Re ` B ) ) )
54 iftrue
 |-  ( x e. A -> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) = ( abs ` ( Im ` B ) ) )
55 53 54 oveq12d
 |-  ( 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 ) ) ) )
56 iftrue
 |-  ( x e. A -> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) = ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) )
57 55 56 eqtr4d
 |-  ( 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 ) )
58 00id
 |-  ( 0 + 0 ) = 0
59 iffalse
 |-  ( -. x e. A -> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) = 0 )
60 iffalse
 |-  ( -. x e. A -> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) = 0 )
61 59 60 oveq12d
 |-  ( -. x e. A -> ( if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) + if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) = ( 0 + 0 ) )
62 iffalse
 |-  ( -. x e. A -> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) = 0 )
63 58 61 62 3eqtr4a
 |-  ( -. 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 ) )
64 57 63 pm2.61i
 |-  ( 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 )
65 64 mpteq2i
 |-  ( 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 ) )
66 52 65 eqtr2di
 |-  ( 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 ) ) oF + ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) ) )
67 66 fveq2d
 |-  ( 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 ) ) oF + ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) ) ) )
68 eqid
 |-  ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) )
69 7 iblcn
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) ) )
70 2 69 mpbid
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
71 70 simpld
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
72 1 2 68 71 32 iblabslem
 |-  ( 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 ) )
73 72 simpld
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) e. MblFn )
74 41 fmpttd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
75 72 simprd
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) ) e. RR )
76 eqid
 |-  ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) )
77 70 simprd
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
78 1 2 76 77 42 iblabslem
 |-  ( 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 ) )
79 78 simpld
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) e. MblFn )
80 49 fmpttd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
81 78 simprd
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` ( Im ` B ) ) , 0 ) ) ) e. RR )
82 73 74 75 79 80 81 itg2add
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( x e. A , ( abs ` ( Re ` B ) ) , 0 ) ) oF + ( 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 ) ) ) ) )
83 67 82 eqtrd
 |-  ( 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 ) ) ) ) )
84 75 81 readdcld
 |-  ( 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 )
85 83 84 eqeltrd
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) ) ) e. RR )
86 34 44 readdcld
 |-  ( ( ph /\ x e. A ) -> ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) e. RR )
87 86 rexrd
 |-  ( ( ph /\ x e. A ) -> ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) e. RR* )
88 34 44 35 45 addge0d
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) )
89 elxrge0
 |-  ( ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) e. ( 0 [,] +oo ) <-> ( ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) e. RR* /\ 0 <_ ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) ) )
90 87 88 89 sylanbrc
 |-  ( ( ph /\ x e. A ) -> ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) e. ( 0 [,] +oo ) )
91 90 26 ifclda
 |-  ( ph -> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) e. ( 0 [,] +oo ) )
92 91 adantr
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) e. ( 0 [,] +oo ) )
93 92 fmpttd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
94 ax-icn
 |-  _i e. CC
95 mulcl
 |-  ( ( _i e. CC /\ ( Im ` B ) e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
96 94 43 95 sylancr
 |-  ( ( ph /\ x e. A ) -> ( _i x. ( Im ` B ) ) e. CC )
97 33 96 abstrid
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) ) <_ ( ( abs ` ( Re ` B ) ) + ( abs ` ( _i x. ( Im ` B ) ) ) ) )
98 7 replimd
 |-  ( ( ph /\ x e. A ) -> B = ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) )
99 98 fveq2d
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) = ( abs ` ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) ) )
100 absmul
 |-  ( ( _i e. CC /\ ( Im ` B ) e. CC ) -> ( abs ` ( _i x. ( Im ` B ) ) ) = ( ( abs ` _i ) x. ( abs ` ( Im ` B ) ) ) )
101 94 43 100 sylancr
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( _i x. ( Im ` B ) ) ) = ( ( abs ` _i ) x. ( abs ` ( Im ` B ) ) ) )
102 absi
 |-  ( abs ` _i ) = 1
103 102 oveq1i
 |-  ( ( abs ` _i ) x. ( abs ` ( Im ` B ) ) ) = ( 1 x. ( abs ` ( Im ` B ) ) )
104 44 recnd
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( Im ` B ) ) e. CC )
105 104 mulid2d
 |-  ( ( ph /\ x e. A ) -> ( 1 x. ( abs ` ( Im ` B ) ) ) = ( abs ` ( Im ` B ) ) )
106 103 105 syl5eq
 |-  ( ( ph /\ x e. A ) -> ( ( abs ` _i ) x. ( abs ` ( Im ` B ) ) ) = ( abs ` ( Im ` B ) ) )
107 101 106 eqtr2d
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( Im ` B ) ) = ( abs ` ( _i x. ( Im ` B ) ) ) )
108 107 oveq2d
 |-  ( ( ph /\ x e. A ) -> ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) = ( ( abs ` ( Re ` B ) ) + ( abs ` ( _i x. ( Im ` B ) ) ) ) )
109 97 99 108 3brtr4d
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) <_ ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) )
110 iftrue
 |-  ( x e. A -> if ( x e. A , ( abs ` B ) , 0 ) = ( abs ` B ) )
111 110 adantl
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( abs ` B ) , 0 ) = ( abs ` B ) )
112 56 adantl
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) = ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) )
113 109 111 112 3brtr4d
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( abs ` B ) , 0 ) <_ if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) )
114 113 ex
 |-  ( ph -> ( x e. A -> if ( x e. A , ( abs ` B ) , 0 ) <_ if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) ) )
115 0le0
 |-  0 <_ 0
116 115 a1i
 |-  ( -. x e. A -> 0 <_ 0 )
117 iffalse
 |-  ( -. x e. A -> if ( x e. A , ( abs ` B ) , 0 ) = 0 )
118 116 117 62 3brtr4d
 |-  ( -. x e. A -> if ( x e. A , ( abs ` B ) , 0 ) <_ if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) )
119 114 118 pm2.61d1
 |-  ( ph -> if ( x e. A , ( abs ` B ) , 0 ) <_ if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) )
120 119 ralrimivw
 |-  ( ph -> A. x e. RR if ( x e. A , ( abs ` B ) , 0 ) <_ if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) )
121 eqidd
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) )
122 eqidd
 |-  ( 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 ) ) )
123 31 28 92 121 122 ofrfval2
 |-  ( ph -> ( ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) oR <_ ( 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 ) ) )
124 120 123 mpbird
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( ( abs ` ( Re ` B ) ) + ( abs ` ( Im ` B ) ) ) , 0 ) ) )
125 itg2le
 |-  ( ( ( 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 ) ) oR <_ ( 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 ) ) ) )
126 29 93 124 125 syl3anc
 |-  ( 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 ) ) ) )
127 itg2lecl
 |-  ( ( ( 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 )
128 29 85 126 127 syl3anc
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR )
129 20 22 iblpos
 |-  ( 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 ) ) )
130 19 128 129 mpbir2and
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )