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