Metamath Proof Explorer

Theorem iblabsnc

Description: Choice-free analogue of iblabs . As with ibladdnc , a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017)

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

Proof

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