Metamath Proof Explorer

Theorem iblabslem

Description: Lemma for iblabs . (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 )
iblabs.3 
|- G = ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )
iblabs.4 
|- ( ph -> ( x e. A |-> ( F ` B ) ) e. L^1 )
iblabs.5 
|- ( ( ph /\ x e. A ) -> ( F ` B ) e. RR )
Assertion iblabslem 
|- ( ph -> ( G e. MblFn /\ ( S.2 ` G ) e. RR ) )

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 iblabs.3 
 |-  G = ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )
4 iblabs.4 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) e. L^1 )
5 iblabs.5 
 |-  ( ( ph /\ x e. A ) -> ( F ` B ) e. RR )
6 5 iblrelem 
 |-  ( ph -> ( ( x e. A |-> ( F ` B ) ) e. L^1 <-> ( ( x e. A |-> ( F ` B ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) e. RR ) ) )
7 4 6 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( F ` B ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) e. RR ) )
8 7 simp1d 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) e. MblFn )
9 8 5 mbfdm2 
 |-  ( ph -> A e. dom vol )
10 mblss 
 |-  ( A e. dom vol -> A C_ RR )
11 9 10 syl 
 |-  ( ph -> A C_ RR )
12 rembl 
 |-  RR e. dom vol
13 12 a1i 
 |-  ( ph -> RR e. dom vol )
14 iftrue 
 |-  ( x e. A -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) = ( abs ` ( F ` B ) ) )
15 14 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) = ( abs ` ( F ` B ) ) )
16 5 recnd 
 |-  ( ( ph /\ x e. A ) -> ( F ` B ) e. CC )
17 16 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( F ` B ) ) e. RR )
18 15 17 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) e. RR )
19 eldifn 
 |-  ( x e. ( RR \ A ) -> -. x e. A )
20 19 adantl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
21 iffalse 
 |-  ( -. x e. A -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) = 0 )
22 20 21 syl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) = 0 )
23 14 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) = ( x e. A |-> ( abs ` ( F ` B ) ) )
24 absf 
 |-  abs : CC --> RR
25 24 a1i 
 |-  ( ph -> abs : CC --> RR )
26 25 16 cofmpt 
 |-  ( ph -> ( abs o. ( x e. A |-> ( F ` B ) ) ) = ( x e. A |-> ( abs ` ( F ` B ) ) ) )
27 23 26 eqtr4id 
 |-  ( ph -> ( x e. A |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) = ( abs o. ( x e. A |-> ( F ` B ) ) ) )
28 16 fmpttd 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) : A --> CC )
29 ax-resscn 
 |-  RR C_ CC
30 ssid 
 |-  CC C_ CC
31 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( CC -cn-> RR ) C_ ( CC -cn-> CC ) )
32 29 30 31 mp2an 
 |-  ( CC -cn-> RR ) C_ ( CC -cn-> CC )
33 abscncf 
 |-  abs e. ( CC -cn-> RR )
34 32 33 sselii 
 |-  abs e. ( CC -cn-> CC )
35 34 a1i 
 |-  ( ph -> abs e. ( CC -cn-> CC ) )
36 cncombf 
 |-  ( ( ( x e. A |-> ( F ` B ) ) e. MblFn /\ ( x e. A |-> ( F ` B ) ) : A --> CC /\ abs e. ( CC -cn-> CC ) ) -> ( abs o. ( x e. A |-> ( F ` B ) ) ) e. MblFn )
37 8 28 35 36 syl3anc 
 |-  ( ph -> ( abs o. ( x e. A |-> ( F ` B ) ) ) e. MblFn )
38 27 37 eqeltrd 
 |-  ( ph -> ( x e. A |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) e. MblFn )
39 11 13 18 22 38 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) e. MblFn )
40 3 39 eqeltrid 
 |-  ( ph -> G e. MblFn )
41 reex 
 |-  RR e. _V
42 41 a1i 
 |-  ( ph -> RR e. _V )
43 ifan 
 |-  if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) = if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 )
44 0re 
 |-  0 e. RR
45 ifcl 
 |-  ( ( ( F ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. RR )
46 5 44 45 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. RR )
47 max1 
 |-  ( ( 0 e. RR /\ ( F ` B ) e. RR ) -> 0 <_ if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
48 44 5 47 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
49 elrege0 
 |-  ( if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. RR /\ 0 <_ if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) ) )
50 46 48 49 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
51 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
52 51 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
53 50 52 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) e. ( 0 [,) +oo ) )
54 43 53 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
55 54 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
56 ifan 
 |-  if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) = if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 )
57 5 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( F ` B ) e. RR )
58 ifcl 
 |-  ( ( -u ( F ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. RR )
59 57 44 58 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. RR )
60 max1 
 |-  ( ( 0 e. RR /\ -u ( F ` B ) e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) )
61 44 57 60 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) )
62 elrege0 
 |-  ( if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) <-> ( if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. RR /\ 0 <_ if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) )
63 59 61 62 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
64 63 52 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) e. ( 0 [,) +oo ) )
65 56 64 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
66 65 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
67 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) )
68 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) )
69 42 55 66 67 68 offval2 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) = ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) + if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) )
70 43 56 oveq12i 
 |-  ( if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) + if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) = ( if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) + if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) )
71 max0add 
 |-  ( ( F ` B ) e. RR -> ( if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) + if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) = ( abs ` ( F ` B ) ) )
72 5 71 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) + if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) = ( abs ` ( F ` B ) ) )
73 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) = if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
74 73 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) = if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
75 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) = if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) )
76 75 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) = if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) )
77 74 76 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) + if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) ) = ( if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) + if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) )
78 72 77 15 3eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) + if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) ) = if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )
79 78 ex 
 |-  ( ph -> ( x e. A -> ( if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) + if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) ) = if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) )
80 00id 
 |-  ( 0 + 0 ) = 0
81 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) = 0 )
82 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) = 0 )
83 81 82 oveq12d 
 |-  ( -. x e. A -> ( if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) + if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) ) = ( 0 + 0 ) )
84 80 83 21 3eqtr4a 
 |-  ( -. x e. A -> ( if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) + if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) ) = if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )
85 79 84 pm2.61d1 
 |-  ( ph -> ( if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) + if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) ) = if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )
86 70 85 syl5eq 
 |-  ( ph -> ( if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) + if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) = if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )
87 86 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> ( if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) + if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) )
88 69 87 eqtrd 
 |-  ( ph -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) )
89 3 88 eqtr4id 
 |-  ( ph -> G = ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) )
90 89 fveq2d 
 |-  ( ph -> ( S.2 ` G ) = ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) ) )
91 54 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
92 43 81 syl5eq 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) = 0 )
93 20 92 syl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) = 0 )
94 ibar 
 |-  ( x e. A -> ( 0 <_ ( F ` B ) <-> ( x e. A /\ 0 <_ ( F ` B ) ) ) )
95 94 ifbid 
 |-  ( x e. A -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) )
96 95 mpteq2ia 
 |-  ( x e. A |-> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) ) = ( x e. A |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) )
97 5 8 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) ) e. MblFn )
98 96 97 eqeltrrid 
 |-  ( ph -> ( x e. A |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) e. MblFn )
99 11 13 91 93 98 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) e. MblFn )
100 55 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
101 7 simp2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) ) e. RR )
102 65 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
103 56 82 syl5eq 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) = 0 )
104 20 103 syl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) = 0 )
105 ibar 
 |-  ( x e. A -> ( 0 <_ -u ( F ` B ) <-> ( x e. A /\ 0 <_ -u ( F ` B ) ) ) )
106 105 ifbid 
 |-  ( x e. A -> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) )
107 106 mpteq2ia 
 |-  ( x e. A |-> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) = ( x e. A |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) )
108 5 8 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( F ` B ) ) e. MblFn )
109 57 108 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) e. MblFn )
110 107 109 eqeltrrid 
 |-  ( ph -> ( x e. A |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) e. MblFn )
111 11 13 102 104 110 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) e. MblFn )
112 66 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
113 7 simp3d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) e. RR )
114 99 100 101 111 112 113 itg2add 
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) oF + ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) ) )
115 90 114 eqtrd 
 |-  ( ph -> ( S.2 ` G ) = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) ) )
116 101 113 readdcld 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) ) e. RR )
117 115 116 eqeltrd 
 |-  ( ph -> ( S.2 ` G ) e. RR )
118 40 117 jca 
 |-  ( ph -> ( G e. MblFn /\ ( S.2 ` G ) e. RR ) )