Metamath Proof Explorer

Theorem iblabsnclem

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

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 iblabsnclem.1 
 |-  G = ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )
4 iblabsnclem.2 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) e. L^1 )
5 iblabsnclem.3 
 |-  ( ( 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 5 recnd 
 |-  ( ( ph /\ x e. A ) -> ( F ` B ) e. CC )
15 14 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( F ` B ) ) e. RR )
16 0re 
 |-  0 e. RR
17 ifcl 
 |-  ( ( ( abs ` ( F ` B ) ) e. RR /\ 0 e. RR ) -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) e. RR )
18 15 16 17 sylancl 
 |-  ( ( 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 iftrue 
 |-  ( x e. A -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) = ( abs ` ( F ` B ) ) )
24 23 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) = ( x e. A |-> ( abs ` ( F ` B ) ) )
25 15 fmpttd 
 |-  ( ph -> ( x e. A |-> ( abs ` ( F ` B ) ) ) : A --> RR )
26 15 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( abs ` ( F ` B ) ) e. RR )
27 26 biantrurd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( y < ( abs ` ( F ` B ) ) <-> ( ( abs ` ( F ` B ) ) e. RR /\ y < ( abs ` ( F ` B ) ) ) ) )
28 5 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( F ` B ) e. RR )
29 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> y e. RR )
30 28 29 absled 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) <_ y <-> ( -u y <_ ( F ` B ) /\ ( F ` B ) <_ y ) ) )
31 30 notbid 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( -. ( abs ` ( F ` B ) ) <_ y <-> -. ( -u y <_ ( F ` B ) /\ ( F ` B ) <_ y ) ) )
32 29 26 ltnled 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( y < ( abs ` ( F ` B ) ) <-> -. ( abs ` ( F ` B ) ) <_ y ) )
33 renegcl 
 |-  ( y e. RR -> -u y e. RR )
34 33 rexrd 
 |-  ( y e. RR -> -u y e. RR* )
35 34 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> -u y e. RR* )
36 elioomnf 
 |-  ( -u y e. RR* -> ( ( F ` B ) e. ( -oo (,) -u y ) <-> ( ( F ` B ) e. RR /\ ( F ` B ) < -u y ) ) )
37 35 36 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F ` B ) e. ( -oo (,) -u y ) <-> ( ( F ` B ) e. RR /\ ( F ` B ) < -u y ) ) )
38 28 biantrurd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F ` B ) < -u y <-> ( ( F ` B ) e. RR /\ ( F ` B ) < -u y ) ) )
39 29 renegcld 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> -u y e. RR )
40 28 39 ltnled 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F ` B ) < -u y <-> -. -u y <_ ( F ` B ) ) )
41 37 38 40 3bitr2d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F ` B ) e. ( -oo (,) -u y ) <-> -. -u y <_ ( F ` B ) ) )
42 rexr 
 |-  ( y e. RR -> y e. RR* )
43 42 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> y e. RR* )
44 elioopnf 
 |-  ( y e. RR* -> ( ( F ` B ) e. ( y (,) +oo ) <-> ( ( F ` B ) e. RR /\ y < ( F ` B ) ) ) )
45 43 44 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F ` B ) e. ( y (,) +oo ) <-> ( ( F ` B ) e. RR /\ y < ( F ` B ) ) ) )
46 28 biantrurd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( y < ( F ` B ) <-> ( ( F ` B ) e. RR /\ y < ( F ` B ) ) ) )
47 29 28 ltnled 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( y < ( F ` B ) <-> -. ( F ` B ) <_ y ) )
48 45 46 47 3bitr2d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F ` B ) e. ( y (,) +oo ) <-> -. ( F ` B ) <_ y ) )
49 41 48 orbi12d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( ( F ` B ) e. ( -oo (,) -u y ) \/ ( F ` B ) e. ( y (,) +oo ) ) <-> ( -. -u y <_ ( F ` B ) \/ -. ( F ` B ) <_ y ) ) )
50 ianor 
 |-  ( -. ( -u y <_ ( F ` B ) /\ ( F ` B ) <_ y ) <-> ( -. -u y <_ ( F ` B ) \/ -. ( F ` B ) <_ y ) )
51 49 50 bitr4di 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( ( F ` B ) e. ( -oo (,) -u y ) \/ ( F ` B ) e. ( y (,) +oo ) ) <-> -. ( -u y <_ ( F ` B ) /\ ( F ` B ) <_ y ) ) )
52 31 32 51 3bitr4rd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( ( F ` B ) e. ( -oo (,) -u y ) \/ ( F ` B ) e. ( y (,) +oo ) ) <-> y < ( abs ` ( F ` B ) ) ) )
53 elioopnf 
 |-  ( y e. RR* -> ( ( abs ` ( F ` B ) ) e. ( y (,) +oo ) <-> ( ( abs ` ( F ` B ) ) e. RR /\ y < ( abs ` ( F ` B ) ) ) ) )
54 43 53 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) e. ( y (,) +oo ) <-> ( ( abs ` ( F ` B ) ) e. RR /\ y < ( abs ` ( F ` B ) ) ) ) )
55 27 52 54 3bitr4rd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) e. ( y (,) +oo ) <-> ( ( F ` B ) e. ( -oo (,) -u y ) \/ ( F ` B ) e. ( y (,) +oo ) ) ) )
56 55 rabbidva 
 |-  ( ( ph /\ y e. RR ) -> { x e. A | ( abs ` ( F ` B ) ) e. ( y (,) +oo ) } = { x e. A | ( ( F ` B ) e. ( -oo (,) -u y ) \/ ( F ` B ) e. ( y (,) +oo ) ) } )
57 eqid 
 |-  ( x e. A |-> ( abs ` ( F ` B ) ) ) = ( x e. A |-> ( abs ` ( F ` B ) ) )
58 57 mptpreima 
 |-  ( `' ( x e. A |-> ( abs ` ( F ` B ) ) ) " ( y (,) +oo ) ) = { x e. A | ( abs ` ( F ` B ) ) e. ( y (,) +oo ) }
59 eqid 
 |-  ( x e. A |-> ( F ` B ) ) = ( x e. A |-> ( F ` B ) )
60 59 mptpreima 
 |-  ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) = { x e. A | ( F ` B ) e. ( -oo (,) -u y ) }
61 59 mptpreima 
 |-  ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) = { x e. A | ( F ` B ) e. ( y (,) +oo ) }
62 60 61 uneq12i 
 |-  ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) u. ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) ) = ( { x e. A | ( F ` B ) e. ( -oo (,) -u y ) } u. { x e. A | ( F ` B ) e. ( y (,) +oo ) } )
63 unrab 
 |-  ( { x e. A | ( F ` B ) e. ( -oo (,) -u y ) } u. { x e. A | ( F ` B ) e. ( y (,) +oo ) } ) = { x e. A | ( ( F ` B ) e. ( -oo (,) -u y ) \/ ( F ` B ) e. ( y (,) +oo ) ) }
64 62 63 eqtri 
 |-  ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) u. ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) ) = { x e. A | ( ( F ` B ) e. ( -oo (,) -u y ) \/ ( F ` B ) e. ( y (,) +oo ) ) }
65 56 58 64 3eqtr4g 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( x e. A |-> ( abs ` ( F ` B ) ) ) " ( y (,) +oo ) ) = ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) u. ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) ) )
66 iblmbf 
 |-  ( ( x e. A |-> ( F ` B ) ) e. L^1 -> ( x e. A |-> ( F ` B ) ) e. MblFn )
67 4 66 syl 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) e. MblFn )
68 5 fmpttd 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) : A --> RR )
69 mbfima 
 |-  ( ( ( x e. A |-> ( F ` B ) ) e. MblFn /\ ( x e. A |-> ( F ` B ) ) : A --> RR ) -> ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) e. dom vol )
70 mbfima 
 |-  ( ( ( x e. A |-> ( F ` B ) ) e. MblFn /\ ( x e. A |-> ( F ` B ) ) : A --> RR ) -> ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) e. dom vol )
71 unmbl 
 |-  ( ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) e. dom vol /\ ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) e. dom vol ) -> ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) u. ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) ) e. dom vol )
72 69 70 71 syl2anc 
 |-  ( ( ( x e. A |-> ( F ` B ) ) e. MblFn /\ ( x e. A |-> ( F ` B ) ) : A --> RR ) -> ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) u. ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) ) e. dom vol )
73 67 68 72 syl2anc 
 |-  ( ph -> ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) u. ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) ) e. dom vol )
74 73 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( ( `' ( x e. A |-> ( F ` B ) ) " ( -oo (,) -u y ) ) u. ( `' ( x e. A |-> ( F ` B ) ) " ( y (,) +oo ) ) ) e. dom vol )
75 65 74 eqeltrd 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( x e. A |-> ( abs ` ( F ` B ) ) ) " ( y (,) +oo ) ) e. dom vol )
76 elioomnf 
 |-  ( y e. RR* -> ( ( abs ` ( F ` B ) ) e. ( -oo (,) y ) <-> ( ( abs ` ( F ` B ) ) e. RR /\ ( abs ` ( F ` B ) ) < y ) ) )
77 43 76 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) e. ( -oo (,) y ) <-> ( ( abs ` ( F ` B ) ) e. RR /\ ( abs ` ( F ` B ) ) < y ) ) )
78 26 biantrurd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) < y <-> ( ( abs ` ( F ` B ) ) e. RR /\ ( abs ` ( F ` B ) ) < y ) ) )
79 28 29 absltd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) < y <-> ( -u y < ( F ` B ) /\ ( F ` B ) < y ) ) )
80 77 78 79 3bitr2d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) e. ( -oo (,) y ) <-> ( -u y < ( F ` B ) /\ ( F ` B ) < y ) ) )
81 28 biantrurd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( -u y < ( F ` B ) /\ ( F ` B ) < y ) <-> ( ( F ` B ) e. RR /\ ( -u y < ( F ` B ) /\ ( F ` B ) < y ) ) ) )
82 80 81 bitrd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) e. ( -oo (,) y ) <-> ( ( F ` B ) e. RR /\ ( -u y < ( F ` B ) /\ ( F ` B ) < y ) ) ) )
83 3anass 
 |-  ( ( ( F ` B ) e. RR /\ -u y < ( F ` B ) /\ ( F ` B ) < y ) <-> ( ( F ` B ) e. RR /\ ( -u y < ( F ` B ) /\ ( F ` B ) < y ) ) )
84 82 83 bitr4di 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) e. ( -oo (,) y ) <-> ( ( F ` B ) e. RR /\ -u y < ( F ` B ) /\ ( F ` B ) < y ) ) )
85 elioo2 
 |-  ( ( -u y e. RR* /\ y e. RR* ) -> ( ( F ` B ) e. ( -u y (,) y ) <-> ( ( F ` B ) e. RR /\ -u y < ( F ` B ) /\ ( F ` B ) < y ) ) )
86 34 42 85 syl2anc 
 |-  ( y e. RR -> ( ( F ` B ) e. ( -u y (,) y ) <-> ( ( F ` B ) e. RR /\ -u y < ( F ` B ) /\ ( F ` B ) < y ) ) )
87 86 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( F ` B ) e. ( -u y (,) y ) <-> ( ( F ` B ) e. RR /\ -u y < ( F ` B ) /\ ( F ` B ) < y ) ) )
88 84 87 bitr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` ( F ` B ) ) e. ( -oo (,) y ) <-> ( F ` B ) e. ( -u y (,) y ) ) )
89 88 rabbidva 
 |-  ( ( ph /\ y e. RR ) -> { x e. A | ( abs ` ( F ` B ) ) e. ( -oo (,) y ) } = { x e. A | ( F ` B ) e. ( -u y (,) y ) } )
90 57 mptpreima 
 |-  ( `' ( x e. A |-> ( abs ` ( F ` B ) ) ) " ( -oo (,) y ) ) = { x e. A | ( abs ` ( F ` B ) ) e. ( -oo (,) y ) }
91 59 mptpreima 
 |-  ( `' ( x e. A |-> ( F ` B ) ) " ( -u y (,) y ) ) = { x e. A | ( F ` B ) e. ( -u y (,) y ) }
92 89 90 91 3eqtr4g 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( x e. A |-> ( abs ` ( F ` B ) ) ) " ( -oo (,) y ) ) = ( `' ( x e. A |-> ( F ` B ) ) " ( -u y (,) y ) ) )
93 mbfima 
 |-  ( ( ( x e. A |-> ( F ` B ) ) e. MblFn /\ ( x e. A |-> ( F ` B ) ) : A --> RR ) -> ( `' ( x e. A |-> ( F ` B ) ) " ( -u y (,) y ) ) e. dom vol )
94 67 68 93 syl2anc 
 |-  ( ph -> ( `' ( x e. A |-> ( F ` B ) ) " ( -u y (,) y ) ) e. dom vol )
95 94 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( x e. A |-> ( F ` B ) ) " ( -u y (,) y ) ) e. dom vol )
96 92 95 eqeltrd 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( x e. A |-> ( abs ` ( F ` B ) ) ) " ( -oo (,) y ) ) e. dom vol )
97 25 9 75 96 ismbf2d 
 |-  ( ph -> ( x e. A |-> ( abs ` ( F ` B ) ) ) e. MblFn )
98 24 97 eqeltrid 
 |-  ( ph -> ( x e. A |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) e. MblFn )
99 11 13 18 22 98 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) ) e. MblFn )
100 3 99 eqeltrid 
 |-  ( ph -> G e. MblFn )
101 reex 
 |-  RR e. _V
102 101 a1i 
 |-  ( ph -> RR e. _V )
103 ifan 
 |-  if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) = if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 )
104 ifcl 
 |-  ( ( ( F ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. RR )
105 5 16 104 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. RR )
106 max1 
 |-  ( ( 0 e. RR /\ ( F ` B ) e. RR ) -> 0 <_ if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
107 16 5 106 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
108 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 ) ) )
109 105 107 108 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
110 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
111 110 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
112 109 111 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) e. ( 0 [,) +oo ) )
113 103 112 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
114 113 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
115 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 )
116 5 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( F ` B ) e. RR )
117 ifcl 
 |-  ( ( -u ( F ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. RR )
118 116 16 117 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. RR )
119 max1 
 |-  ( ( 0 e. RR /\ -u ( F ` B ) e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) )
120 16 116 119 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) )
121 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 ) ) )
122 118 120 121 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
123 122 111 ifclda 
 |-  ( ph -> if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) e. ( 0 [,) +oo ) )
124 115 123 eqeltrid 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
125 124 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
126 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 ) ) )
127 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 ) ) )
128 102 114 125 126 127 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 ) ) ) )
129 103 115 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 ) )
130 max0add 
 |-  ( ( F ` B ) e. RR -> ( if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) + if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) = ( abs ` ( F ` B ) ) )
131 5 130 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) + if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) ) = ( abs ` ( F ` B ) ) )
132 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) = if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
133 132 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) = if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) )
134 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 ) )
135 134 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 ) )
136 133 135 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 ) ) )
137 23 adantl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) = ( abs ` ( F ` B ) ) )
138 131 136 137 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 ) )
139 138 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 ) ) )
140 00id 
 |-  ( 0 + 0 ) = 0
141 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) , 0 ) = 0 )
142 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ -u ( F ` B ) , -u ( F ` B ) , 0 ) , 0 ) = 0 )
143 141 142 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 ) )
144 140 143 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 ) )
145 139 144 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 ) )
146 129 145 eqtrid 
 |-  ( 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 ) )
147 146 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 ) ) )
148 128 147 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 ) ) )
149 3 148 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 ) ) ) )
150 149 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 ) ) ) ) )
151 113 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) e. ( 0 [,) +oo ) )
152 103 141 eqtrid 
 |-  ( -. x e. A -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) = 0 )
153 20 152 syl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) = 0 )
154 ibar 
 |-  ( x e. A -> ( 0 <_ ( F ` B ) <-> ( x e. A /\ 0 <_ ( F ` B ) ) ) )
155 154 ifbid 
 |-  ( x e. A -> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) )
156 155 mpteq2ia 
 |-  ( x e. A |-> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) ) = ( x e. A |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) )
157 5 8 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( F ` B ) , ( F ` B ) , 0 ) ) e. MblFn )
158 156 157 eqeltrrid 
 |-  ( ph -> ( x e. A |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) e. MblFn )
159 11 13 151 153 158 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) e. MblFn )
160 114 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
161 7 simp2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( F ` B ) ) , ( F ` B ) , 0 ) ) ) e. RR )
162 125 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) : RR --> ( 0 [,) +oo ) )
163 7 simp3d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( F ` B ) ) , -u ( F ` B ) , 0 ) ) ) e. RR )
164 159 160 161 162 163 itg2addnc 
 |-  ( 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 ) ) ) ) )
165 150 164 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 ) ) ) ) )
166 161 163 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 )
167 165 166 eqeltrd 
 |-  ( ph -> ( S.2 ` G ) e. RR )
168 100 167 jca 
 |-  ( ph -> ( G e. MblFn /\ ( S.2 ` G ) e. RR ) )