Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1anclem5 Structured version   Unicode version

Theorem ftc1anclem5 31941
Description: Lemma for ftc1anc 31945, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.)
Hypotheses
Ref Expression
ftc1anc.g  |-  G  =  ( x  e.  ( A [,] B ) 
|->  S. ( A (,) x ) ( F `
 t )  _d t )
ftc1anc.a  |-  ( ph  ->  A  e.  RR )
ftc1anc.b  |-  ( ph  ->  B  e.  RR )
ftc1anc.le  |-  ( ph  ->  A  <_  B )
ftc1anc.s  |-  ( ph  ->  ( A (,) B
)  C_  D )
ftc1anc.d  |-  ( ph  ->  D  C_  RR )
ftc1anc.i  |-  ( ph  ->  F  e.  L^1 )
ftc1anc.f  |-  ( ph  ->  F : D --> CC )
Assertion
Ref Expression
ftc1anclem5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  E. f  e.  dom  S.1 ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  ( f `
 t ) ) ) ) )  < 
Y )
Distinct variable groups:    t, f, x, A    B, f, t, x    D, f, t, x   
f, F, t, x    ph, f, t, x    f, G    f, Y, t, x
Allowed substitution hints:    G( x, t)

Proof of Theorem ftc1anclem5
Dummy variable  g is distinct from all other variables.
StepHypRef Expression
1 iftrue 3916 . . . . . . . . 9  |-  ( t  e.  RR  ->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 )  =  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )
21mpteq2ia 4504 . . . . . . . 8  |-  ( t  e.  RR  |->  if ( t  e.  RR , 
( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) )  =  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )
32fveq2i 5882 . . . . . . 7  |-  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) ) )  =  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )
4 ftc1anc.f . . . . . . . . . . . . . 14  |-  ( ph  ->  F : D --> CC )
54ffvelrnda 6035 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  D )  ->  ( F `  t )  e.  CC )
6 0cnd 9638 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  t  e.  D )  ->  0  e.  CC )
75, 6ifclda 3942 . . . . . . . . . . . 12  |-  ( ph  ->  if ( t  e.  D ,  ( F `
 t ) ,  0 )  e.  CC )
87recld 13251 . . . . . . . . . . 11  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
98adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  RR )
10 ftc1anc.d . . . . . . . . . . 11  |-  ( ph  ->  D  C_  RR )
11 rembl 22486 . . . . . . . . . . . 12  |-  RR  e.  dom  vol
1211a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  dom  vol )
138adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  D )  ->  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  e.  RR )
14 eldifn 3589 . . . . . . . . . . . . 13  |-  ( t  e.  ( RR  \  D )  ->  -.  t  e.  D )
1514adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( RR  \  D ) )  ->  -.  t  e.  D )
16 iffalse 3919 . . . . . . . . . . . . . 14  |-  ( -.  t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  0 )
1716fveq2d 5883 . . . . . . . . . . . . 13  |-  ( -.  t  e.  D  -> 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  ( Re `  0 ) )
18 re0 13209 . . . . . . . . . . . . 13  |-  ( Re
`  0 )  =  0
1917, 18syl6eq 2480 . . . . . . . . . . . 12  |-  ( -.  t  e.  D  -> 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  =  0 )
2015, 19syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( RR  \  D ) )  ->  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) )  =  0 )
21 iftrue 3916 . . . . . . . . . . . . . 14  |-  ( t  e.  D  ->  if ( t  e.  D ,  ( F `  t ) ,  0 )  =  ( F `
 t ) )
2221fveq2d 5883 . . . . . . . . . . . . 13  |-  ( t  e.  D  ->  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) )  =  ( Re
`  ( F `  t ) ) )
2322mpteq2ia 4504 . . . . . . . . . . . 12  |-  ( t  e.  D  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  =  ( t  e.  D  |->  ( Re
`  ( F `  t ) ) )
244feqmptd 5932 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  =  ( t  e.  D  |->  ( F `
 t ) ) )
25 ftc1anc.i . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  L^1 )
2624, 25eqeltrrd 2512 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e.  L^1 )
275iblcn 22748 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( t  e.  D  |->  ( F `  t ) )  e.  L^1  <->  ( (
t  e.  D  |->  ( Re `  ( F `
 t ) ) )  e.  L^1 
/\  ( t  e.  D  |->  ( Im `  ( F `  t ) ) )  e.  L^1 ) ) )
2826, 27mpbid 214 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( t  e.  D  |->  ( Re `  ( F `  t ) ) )  e.  L^1  /\  ( t  e.  D  |->  ( Im `  ( F `  t ) ) )  e.  L^1 ) )
2928simpld 461 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e.  L^1 )
3023, 29syl5eqel 2515 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  L^1 )
3110, 12, 13, 20, 30iblss2 22755 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  L^1 )
328recnd 9671 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
3332adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  RR )  ->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC )
34 eqidd 2424 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  =  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )
35 absf 13394 . . . . . . . . . . . . . 14  |-  abs : CC
--> RR
3635a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  abs : CC --> RR )
3736feqmptd 5932 . . . . . . . . . . . 12  |-  ( ph  ->  abs  =  ( x  e.  CC  |->  ( abs `  x ) ) )
38 fveq2 5879 . . . . . . . . . . . 12  |-  ( x  =  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  ->  ( abs `  x )  =  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )
3933, 34, 37, 38fmptco 6069 . . . . . . . . . . 11  |-  ( ph  ->  ( abs  o.  (
t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )
40 eqid 2423 . . . . . . . . . . . . 13  |-  ( t  e.  RR  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  =  ( t  e.  RR  |->  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
419, 40fmptd 6059 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) : RR --> RR )
42 iblmbf 22717 . . . . . . . . . . . . . . . . . 18  |-  ( F  e.  L^1  ->  F  e. MblFn )
4325, 42syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  e. MblFn )
4424, 43eqeltrrd 2512 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( t  e.  D  |->  ( F `  t
) )  e. MblFn )
455ismbfcn2 22587 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( t  e.  D  |->  ( F `  t ) )  e. MblFn  <->  ( ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e. MblFn  /\  (
t  e.  D  |->  ( Im `  ( F `
 t ) ) )  e. MblFn ) ) )
4644, 45mpbid 214 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( t  e.  D  |->  ( Re `  ( F `  t ) ) )  e. MblFn  /\  (
t  e.  D  |->  ( Im `  ( F `
 t ) ) )  e. MblFn ) )
4746simpld 461 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  ( F `  t )
) )  e. MblFn )
4823, 47syl5eqel 2515 . . . . . . . . . . . . 13  |-  ( ph  ->  ( t  e.  D  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. MblFn
)
4910, 12, 13, 20, 48mbfss 22594 . . . . . . . . . . . 12  |-  ( ph  ->  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) )  e. MblFn )
50 ftc1anclem1 31937 . . . . . . . . . . . 12  |-  ( ( ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) : RR --> RR  /\  ( t  e.  RR  |->  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. MblFn
)  ->  ( abs  o.  ( t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e. MblFn
)
5141, 49, 50syl2anc 666 . . . . . . . . . . 11  |-  ( ph  ->  ( abs  o.  (
t  e.  RR  |->  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e. MblFn
)
5239, 51eqeltrrd 2512 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e. MblFn )
539, 31, 52iblabsnc 31926 . . . . . . . . 9  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e.  L^1 )
5432abscld 13491 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  RR )
5554adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  RR )
5632absge0d 13499 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )
5756adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  RR )  ->  0  <_ 
( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )
5855, 57iblpos 22742 . . . . . . . . 9  |-  ( ph  ->  ( ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e.  L^1  <->  ( (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  e. MblFn  /\  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ,  0 ) ) )  e.  RR ) ) )
5953, 58mpbid 214 . . . . . . . 8  |-  ( ph  ->  ( ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  e. MblFn  /\  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) ) )  e.  RR ) )
6059simprd 465 . . . . . . 7  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  if ( t  e.  RR ,  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ,  0 ) ) )  e.  RR )
613, 60syl5eqelr 2516 . . . . . 6  |-  ( ph  ->  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR )
62 ltsubrp 11337 . . . . . 6  |-  ( ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) ) )
6361, 62sylan 474 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  < 
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) ) )
64 rpre 11310 . . . . . . 7  |-  ( Y  e.  RR+  ->  Y  e.  RR )
65 resubcl 9940 . . . . . . 7  |-  ( ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR  /\  Y  e.  RR )  ->  (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR )
6661, 64, 65syl2an 480 . . . . . 6  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  e.  RR )
6761adantr 467 . . . . . 6  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  e.  RR )
6866, 67ltnled 9784 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  <->  -.  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
6963, 68mpbid 214 . . . 4  |-  ( (
ph  /\  Y  e.  RR+ )  ->  -.  ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) )
7054rexrd 9692 . . . . . . . . 9  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  RR* )
71 elxrge0 11743 . . . . . . . . 9  |-  ( ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  ( 0 [,] +oo )  <->  ( ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e. 
RR*  /\  0  <_  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )
7270, 56, 71sylanbrc 669 . . . . . . . 8  |-  ( ph  ->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) )  e.  ( 0 [,] +oo )
)
7372adantr 467 . . . . . . 7  |-  ( (
ph  /\  t  e.  RR )  ->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )  e.  ( 0 [,] +oo ) )
74 eqid 2423 . . . . . . 7  |-  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) )  =  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )
7573, 74fmptd 6059 . . . . . 6  |-  ( ph  ->  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
7675adantr 467 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo ) )
7766rexrd 9692 . . . . 5  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  e. 
RR* )
78 itg2leub 22684 . . . . 5  |-  ( ( ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) : RR --> ( 0 [,] +oo )  /\  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR* )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  <_ 
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <->  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) ) )
7976, 77, 78syl2anc 666 . . . 4  |-  ( (
ph  /\  Y  e.  RR+ )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <->  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) ) )
8069, 79mtbid 302 . . 3  |-  ( (
ph  /\  Y  e.  RR+ )  ->  -.  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
81 rexanali 2879 . . 3  |-  ( E. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  <->  -.  A. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  -> 
( S.1 `  g )  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
8280, 81sylibr 216 . 2  |-  ( (
ph  /\  Y  e.  RR+ )  ->  E. g  e.  dom  S.1 ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) ) )
8366ad2antrr 731 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR )
84 itg1cl 22635 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  e.  RR )
8584ad2antlr 732 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( S.1 `  g
)  e.  RR )
86 eqid 2423 . . . . . . . . . . . 12  |-  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  =  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
8786i1fpos 22656 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 )
88 0re 9645 . . . . . . . . . . . . . 14  |-  0  e.  RR
89 i1ff 22626 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  g : RR --> RR )
9089ffvelrnda 6035 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  e.  RR )
91 max1 11482 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  ( g `  t
)  e.  RR )  ->  0  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
9288, 90, 91sylancr 668 . . . . . . . . . . . . 13  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
9392ralrimiva 2840 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
94 ax-resscn 9598 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
9594a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  RR  C_  CC )
96 fvex 5889 . . . . . . . . . . . . . . . . 17  |-  ( g `
 t )  e. 
_V
97 c0ex 9639 . . . . . . . . . . . . . . . . 17  |-  0  e.  _V
9896, 97ifex 3978 . . . . . . . . . . . . . . . 16  |-  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e. 
_V
9998, 86fnmpti 5722 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  Fn  RR
10099a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  Fn  RR )
10195, 1000pledm 22623 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( 0p  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  <-> 
( RR  X.  {
0 } )  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
102 reex 9632 . . . . . . . . . . . . . . 15  |-  RR  e.  _V
103102a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  RR  e.  _V )
10497a1i 11 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  0  e.  _V )
105 ifcl 3952 . . . . . . . . . . . . . . 15  |-  ( ( ( g `  t
)  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 )  e.  RR )
10690, 88, 105sylancl 667 . . . . . . . . . . . . . 14  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  RR )
107 fconstmpt 4895 . . . . . . . . . . . . . . 15  |-  ( RR 
X.  { 0 } )  =  ( t  e.  RR  |->  0 )
108107a1i 11 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  ( RR  X.  { 0 } )  =  ( t  e.  RR  |->  0 ) )
109 eqidd 2424 . . . . . . . . . . . . . 14  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  =  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
110103, 104, 106, 108, 109ofrfval2 6561 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  ( ( RR  X.  {
0 } )  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  <->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )
111101, 110bitrd 257 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  ( 0p  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )  <->  A. t  e.  RR  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )
11293, 111mpbird 236 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  0p  oR  <_ 
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
113 itg2itg1 22686 . . . . . . . . . . 11  |-  ( ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
/\  0p  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  =  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
11487, 112, 113syl2anc 666 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  =  ( S.1 `  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
115 itg1cl 22635 . . . . . . . . . . 11  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
11687, 115syl 17 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.1 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
117114, 116eqeltrd 2511 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
118117ad2antlr 732 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( S.2 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
119 ltnle 9715 . . . . . . . . . 10  |-  ( ( ( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  e.  RR  /\  ( S.1 `  g
)  e.  RR )  ->  ( ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.1 `  g
)  <->  -.  ( S.1 `  g )  <_  (
( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
12066, 84, 119syl2an 480 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  ->  (
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.1 `  g )  <->  -.  ( S.1 `  g )  <_ 
( ( S.2 `  (
t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y ) ) )
121120biimpar 488 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.1 `  g ) )
122 max2 11484 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  ( g `  t
)  e.  RR )  ->  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
12388, 90, 122sylancr 668 . . . . . . . . . . . . 13  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
124123ralrimiva 2840 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  A. t  e.  RR  (
g `  t )  <_  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) )
12589feqmptd 5932 . . . . . . . . . . . . 13  |-  ( g  e.  dom  S.1  ->  g  =  ( t  e.  RR  |->  ( g `  t ) ) )
126103, 90, 106, 125, 109ofrfval2 6561 . . . . . . . . . . . 12  |-  ( g  e.  dom  S.1  ->  ( g  oR  <_ 
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  <->  A. t  e.  RR  ( g `  t )  <_  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
127124, 126mpbird 236 . . . . . . . . . . 11  |-  ( g  e.  dom  S.1  ->  g  oR  <_  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
128 itg1le 22663 . . . . . . . . . . 11  |-  ( ( g  e.  dom  S.1  /\  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
/\  g  oR  <_  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  ->  ( S.1 `  g )  <_  ( S.1 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
12987, 127, 128mpd3an23 1363 . . . . . . . . . 10  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  <_  ( S.1 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
130129, 114breqtrrd 4448 . . . . . . . . 9  |-  ( g  e.  dom  S.1  ->  ( S.1 `  g )  <_  ( S.2 `  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
131130ad2antlr 732 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( S.1 `  g
)  <_  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
13283, 85, 118, 121, 131ltletrd 9797 . . . . . . 7  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ) ) )  -  Y )  <  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
133132adantrl 721 . . . . . 6  |-  ( ( ( ( ph  /\  Y  e.  RR+ )  /\  g  e.  dom  S.1 )  /\  ( g  oR  <_  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) )  /\  -.  ( S.1 `  g
)  <_  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y ) ) )  ->  ( ( S.2 `  ( t  e.  RR  |->  ( abs `  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ) ) )  -  Y )  < 
( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
134 i1fmbf 22625 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e. MblFn )
13587, 134syl 17 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e. MblFn )
136135adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e. MblFn )
137 elrege0 11740 . . . . . . . . . . . . . . . . 17  |-  ( if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  ( 0 [,) +oo )  <->  ( if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  RR  /\  0  <_  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )
138106, 92, 137sylanbrc 669 . . . . . . . . . . . . . . . 16  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  ( 0 [,) +oo ) )
139138, 86fmptd 6059 . . . . . . . . . . . . . . 15  |-  ( g  e.  dom  S.1  ->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
140139adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
141117adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  ( S.2 `  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  RR )
142106recnd 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
143142negcld 9975 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  -u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 )  e.  CC )
144142, 143ifcld 3953 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g  e.  dom  S.1  /\  t  e.  RR )  ->  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  CC )
145 subcl 9876 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  CC  /\  if ( 0  <_ 
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  CC )  ->  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  CC )
14632, 144, 145syl2an 480 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( g  e.  dom  S.1  /\  t  e.  RR ) )  -> 
( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  CC )
147146anassrs 653 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) )  e.  CC )
148147abscld 13491 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  RR )
149147absge0d 13499 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  0  <_  ( abs `  (
( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
150 elrege0 11740 . . . . . . . . . . . . . . . 16  |-  ( ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  ( 0 [,) +oo )  <->  ( ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  RR  /\  0  <_  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) ) )
151148, 149, 150sylanbrc 669 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  g  e.  dom  S.1 )  /\  t  e.  RR )  ->  ( abs `  ( ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )  e.  ( 0 [,) +oo ) )
152 eqid 2423 . . . . . . . . . . . . . . 15  |-  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
153151, 152fmptd 6059 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) ) : RR --> ( 0 [,) +oo ) )
154 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
x  e.  D  <->  t  e.  D ) )
155 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  ( F `  x )  =  ( F `  t ) )
156154, 155ifbieq1d 3933 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( x  e.  D ,  ( F `  x ) ,  0 )  =  if ( t  e.  D , 
( F `  t
) ,  0 ) )
157156fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  t  ->  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
158 eqid 2423 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) )
159 fvex 5889 . . . . . . . . . . . . . . . . . . . 20  |-  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  e.  _V
160157, 158, 159fvmpt 5962 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  =  ( Re
`  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) )
161157breq2d 4433 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  (
0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) )  <->  0  <_  ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) ) ) )
162 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
163162breq2d 4433 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  t  ->  (
0  <_  ( g `  x )  <->  0  <_  ( g `  t ) ) )
164163, 162ifbieq1d 3933 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) )
165164negeqd 9871 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  t  ->  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )
166161, 164, 165ifbieq12d 3937 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  t  ->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  =  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
167 eqid 2423 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )
168 negex 9875 . . . . . . . . . . . . . . . . . . . . 21  |-  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  e.  _V
16998, 168ifex 3978 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  _V
170166, 167, 169fvmpt 5962 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  RR  ->  (
( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t )  =  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) ) ,  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )
171160, 170oveq12d 6321 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  RR  ->  (
( ( x  e.  RR  |->  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  (
( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) )  =  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) )
172171fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  RR  ->  ( abs `  ( ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) ) )  =  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
173172mpteq2ia 4504 . . . . . . . . . . . . . . . 16  |-  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Re
`  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ) `  t )  -  ( ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) ) ) )  =  ( t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  if ( 0  <_  (
Re `  if (
t  e.  D , 
( F `  t
) ,  0 ) ) ,  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) , 
-u if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) )
174173fveq2i 5882 . . . . . . . . . . . . . . 15  |-  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( ( x  e.  RR  |->  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) `  t
)  -  ( ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) `  t ) ) ) ) )  =  ( S.2 `  (
t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D , 
( F `  t
) ,  0 ) )  -  if ( 0  <_  ( Re `  if ( t  e.  D ,  ( F `
 t ) ,  0 ) ) ,  if ( 0  <_ 
( g `  t
) ,  ( g `
 t ) ,  0 ) ,  -u if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) ) ) )
175102a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  e.  _V )
176 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g `
 x )  e. 
_V
177176, 97ifex 3978 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e. 
_V
178177, 97ifex 3978 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 )  e.  _V
179178a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 )  e.  _V )
180 ovex 6331 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  e.  _V
18197, 180ifex 3978 . . . . . . . . . . . . . . . . . . . 20  |-  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )  e.  _V
182181a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR )  ->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )  e.  _V )
183 ffn 5744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  F  Fn  D )
184 frn 5750 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : D --> CC  ->  ran 
F  C_  CC )
185 ref 13169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  Re : CC
--> RR
186 ffn 5744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Re : CC --> RR  ->  Re  Fn  CC )
187185, 186ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  Re  Fn  CC
188 fnco 5700 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Re  Fn  CC  /\  F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
189187, 188mp3an1 1348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F  Fn  D  /\  ran  F  C_  CC )  ->  ( Re  o.  F
)  Fn  D )
190183, 184, 189syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( F : D --> CC  ->  ( Re  o.  F )  Fn  D )
191 elpreima 6015 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( Re  o.  F )  Fn  D  ->  (
x  e.  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  <-> 
( x  e.  D  /\  ( ( Re  o.  F ) `  x
)  e.  ( 0 [,) +oo ) ) ) )
1924, 190, 1913syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( x  e.  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  <->  ( x  e.  D  /\  ( ( Re  o.  F ) `
 x )  e.  ( 0 [,) +oo ) ) ) )
193 fco 5754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Re : CC --> RR  /\  F : D --> CC )  ->  ( Re  o.  F ) : D --> RR )
194185, 4, 193sylancr 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( Re  o.  F
) : D --> RR )
195194ffvelrnda 6035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  e.  RR )
196195biantrurd 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  ( (
( Re  o.  F
) `  x )  e.  RR  /\  0  <_ 
( ( Re  o.  F ) `  x
) ) ) )
197 elrege0 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( Re  o.  F
) `  x )  e.  ( 0 [,) +oo ) 
<->  ( ( ( Re  o.  F ) `  x )  e.  RR  /\  0  <_  ( (
Re  o.  F ) `  x ) ) )
198196, 197syl6bbr 267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  ( (
Re  o.  F ) `  x )  e.  ( 0 [,) +oo )
) )
199 fvco3 5956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F : D --> CC  /\  x  e.  D )  ->  ( ( Re  o.  F ) `  x
)  =  ( Re
`  ( F `  x ) ) )
2004, 199sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  D )  ->  (
( Re  o.  F
) `  x )  =  ( Re `  ( F `  x ) ) )
201200breq2d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  D )  ->  (
0  <_  ( (
Re  o.  F ) `  x )  <->  0  <_  ( Re `  ( F `
 x ) ) ) )
202198, 201bitr3d 259 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  D )  ->  (
( ( Re  o.  F ) `  x
)  e.  ( 0 [,) +oo )  <->  0  <_  ( Re `  ( F `
 x ) ) ) )
203202pm5.32da 646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( x  e.  D  /\  ( ( Re  o.  F ) `
 x )  e.  ( 0 [,) +oo ) )  <->  ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) ) ) )
204192, 203bitrd 257 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( x  e.  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  <->  ( x  e.  D  /\  0  <_ 
( Re `  ( F `  x )
) ) ) )
205204adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  <->  ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) ) ) )
206 0le0 10701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <_  0
207206, 18breqtrri 4447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  <_  ( Re `  0
)
208207biantru 508 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  e.  D  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) )
209 eldif 3447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( RR  \  D )  <->  ( x  e.  RR  /\  -.  x  e.  D ) )
210209baibr 913 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  ->  ( -.  x  e.  D  <->  x  e.  ( RR  \  D ) ) )
211208, 210syl5rbbr 264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  (
x  e.  ( RR 
\  D )  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) ) )
212211adantl 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( RR  \  D )  <->  ( -.  x  e.  D  /\  0  <_  ( Re ` 
0 ) ) ) )
213205, 212orbi12d 715 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  e.  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  \/  x  e.  ( RR  \  D ) )  <->  ( ( x  e.  D  /\  0  <_  ( Re `  ( F `  x )
) )  \/  ( -.  x  e.  D  /\  0  <_  ( Re
`  0 ) ) ) ) )
214 elun 3607 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <->  ( x  e.  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  \/  x  e.  ( RR  \  D
) ) )
215 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x )  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  ( F `
 x ) ) )
216215breq2d 4433 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  ( F `
 x )  -> 
( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  <->  0  <_  (
Re `  ( F `  x ) ) ) )
217 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  =  ( Re `  0 ) )
218217breq2d 4433 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( x  e.  D ,  ( F `  x ) ,  0 )  =  0  -> 
( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) )  <->  0  <_  (
Re `  0 )
) )
219216, 218elimif 3944 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) )  <->  ( (
x  e.  D  /\  0  <_  ( Re `  ( F `  x ) ) )  \/  ( -.  x  e.  D  /\  0  <_  ( Re
`  0 ) ) ) )
220213, 214, 2193bitr4g 292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <->  0  <_  ( Re `  if ( x  e.  D , 
( F `  x
) ,  0 ) ) ) )
221220ifbid 3932 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  =  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )
222221mpteq2dva 4508 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  =  ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) ) )
223220ifbid 3932 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  RR )  ->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )  =  if ( 0  <_ 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )
224223mpteq2dva 4508 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) ) )
225175, 179, 182, 222, 224offval2 6560 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 ) )  oF  +  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) ) )  =  ( x  e.  RR  |->  ( if ( 0  <_ 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) ) ) )
226 ovif12 6387 . . . . . . . . . . . . . . . . . . . 20  |-  ( if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  ( if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) )
22789ffvelrnda 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  RR )
228227recnd 9671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( g `  x )  e.  CC )
229 0cn 9637 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  CC
230 ifcl 3952 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 )  e.  CC )
231228, 229, 230sylancl 667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
232231addid1d 9835 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  +  0 )  =  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) )
233231mulm1d 10072 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) )  = 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
234233oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) )  =  ( 0  + 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )
235231negcld 9975 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 )  e.  CC )
236235addid2d 9836 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( 0  + 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  =  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
237234, 236eqtrd 2464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) )  =  -u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
238232, 237ifeq12d 3930 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  ( if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 )  +  0 ) ,  ( 0  +  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) )  =  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
239226, 238syl5eq 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g  e.  dom  S.1  /\  x  e.  RR )  ->  ( if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  0 ,  ( -u
1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) )  =  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) )
240239mpteq2dva 4508 . . . . . . . . . . . . . . . . . 18  |-  ( g  e.  dom  S.1  ->  ( x  e.  RR  |->  ( if ( 0  <_ 
( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  +  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `  x ) ,  0 ) ) ,  0 ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  (
Re `  if (
x  e.  D , 
( F `  x
) ,  0 ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) , 
-u if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ) ) )
241225, 240sylan9eq 2484 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  g  e.  dom  S.1 )  ->  (
( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  oF  +  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) ) )  =  ( x  e.  RR  |->  if ( 0  <_  ( Re `  if ( x  e.  D ,  ( F `
 x ) ,  0 ) ) ,  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ,  -u if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) )
242 0xr 9689 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
243 pnfxr 11414 . . . . . . . . . . . . . . . . . . . . . . 23  |- +oo  e.  RR*
244 0ltpnf 11426 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  < +oo
245 snunioo 11760 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  < +oo )  ->  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo ) )
246242, 243, 244, 245mp3an 1361 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { 0 }  u.  (
0 (,) +oo )
)  =  ( 0 [,) +oo )
247246imaeq2i 5183 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( `' ( Re  o.  F ) " (
0 [,) +oo )
)
248 imaundi 5265 . . . . . . . . . . . . . . . . . . . . 21  |-  ( `' ( Re  o.  F
) " ( { 0 }  u.  (
0 (,) +oo )
) )  =  ( ( `' ( Re  o.  F ) " { 0 } )  u.  ( `' ( Re  o.  F )
" ( 0 (,) +oo ) ) )
249247, 248eqtr3i 2454 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  =  ( ( `' ( Re  o.  F
) " { 0 } )  u.  ( `' ( Re  o.  F ) " (
0 (,) +oo )
) )
250 ismbfcn 22579 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : D --> CC  ->  ( F  e. MblFn  <->  ( ( Re  o.  F )  e. MblFn  /\  ( Im  o.  F
)  e. MblFn ) )
)
2514, 250syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( F  e. MblFn  <->  ( (
Re  o.  F )  e. MblFn  /\  ( Im  o.  F )  e. MblFn )
) )
25243, 251mpbid 214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( Re  o.  F )  e. MblFn  /\  (
Im  o.  F )  e. MblFn ) )
253252simpld 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Re  o.  F
)  e. MblFn )
254 mbfimasn 22582 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR  /\  0  e.  RR )  ->  ( `' ( Re  o.  F ) " {
0 } )  e. 
dom  vol )
25588, 254mp3an3 1350 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) " { 0 } )  e.  dom  vol )
256 mbfima 22580 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( `' ( Re  o.  F ) "
( 0 (,) +oo ) )  e.  dom  vol )
257 unmbl 22483 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( `' ( Re  o.  F ) " { 0 } )  e.  dom  vol  /\  ( `' ( Re  o.  F ) " (
0 (,) +oo )
)  e.  dom  vol )  ->  ( ( `' ( Re  o.  F
) " { 0 } )  u.  ( `' ( Re  o.  F ) " (
0 (,) +oo )
) )  e.  dom  vol )
258255, 256, 257syl2anc 666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( Re  o.  F
)  e. MblFn  /\  (
Re  o.  F ) : D --> RR )  -> 
( ( `' ( Re  o.  F )
" { 0 } )  u.  ( `' ( Re  o.  F
) " ( 0 (,) +oo ) ) )  e.  dom  vol )
259253, 194, 258syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" { 0 } )  u.  ( `' ( Re  o.  F
) " ( 0 (,) +oo ) ) )  e.  dom  vol )
260249, 259syl5eqel 2515 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  e.  dom  vol )
261 fdm 5748 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : D --> CC  ->  dom 
F  =  D )
2624, 261syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  =  D )
263 mbfdm 22576 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F  e. MblFn  ->  dom  F  e.  dom  vol )
26443, 263syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  F  e.  dom  vol )
265262, 264eqeltrrd 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  D  e.  dom  vol )
266 difmbl 22488 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  e.  dom  vol  /\  D  e.  dom  vol )  ->  ( RR  \  D )  e.  dom  vol )
26711, 265, 266sylancr 668 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  \  D
)  e.  dom  vol )
268 unmbl 22483 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  e.  dom  vol 
/\  ( RR  \  D )  e.  dom  vol )  ->  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) )  e.  dom  vol )
269260, 267, 268syl2anc 666 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e.  dom  vol )
270 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  x  ->  (
g `  t )  =  ( g `  x ) )
271270breq2d 4433 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  x  ->  (
0  <_  ( g `  t )  <->  0  <_  ( g `  x ) ) )
272271, 270ifbieq1d 3933 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  x  ->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 )  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
273272, 86, 177fvmpt 5962 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  (
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
274273eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 )  =  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
) )
275274ifeq1d 3928 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  ->  if ( x  e.  (
( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 )  =  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) `
 x ) ,  0 ) )
276275mpteq2ia 4504 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) `
 x ) ,  0 ) )
277276i1fres 22655 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
/\  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e. 
dom  vol )  ->  (
x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) ,  0 ) )  e. 
dom  S.1 )
278 id 23 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 )
279 neg1rr 10716 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u 1  e.  RR
280279a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  -u 1  e.  RR )
281278, 280i1fmulc 22653 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  e.  dom  S.1 
->  ( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) )  e. 
dom  S.1 )
282 cmmbl 22480 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) )  e.  dom  vol  ->  ( RR  \  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) )  e.  dom  vol )
283 ifnot 3955 . . . . . . . . . . . . . . . . . . . . . . 23  |-  if ( -.  x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ,  0 )  =  if ( x  e.  ( ( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
284 eldif 3447 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( RR  \ 
( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) )  <->  ( x  e.  RR  /\  -.  x  e.  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) )
285284baibr 913 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  ( -.  x  e.  (
( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) )  <-> 
x  e.  ( RR 
\  ( ( `' ( Re  o.  F
) " ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) ) )
286 tru 1442 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |- T.
287 negex 9875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  -u 1  e.  _V
288287fconst 5784 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR 
X.  { -u 1 } ) : RR --> { -u 1 }
289 ffn 5744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( RR  X.  { -u
1 } ) : RR --> { -u 1 }  ->  ( RR  X.  { -u 1 } )  Fn  RR )
290288, 289mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  ( RR  X.  { -u 1 } )  Fn  RR )
29199a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  ( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )  Fn  RR )
292102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( T. 
->  RR  e.  _V )
293 inidm 3672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( RR 
i^i  RR )  =  RR
294287fvconst2 6133 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  RR  ->  (
( RR  X.  { -u 1 } ) `  x )  =  -u
1 )
295294adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T.  /\  x  e.  RR )  ->  (
( RR  X.  { -u 1 } ) `  x )  =  -u
1 )
296273adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T.  /\  x  e.  RR )  ->  (
( t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )
297290, 291, 292, 292, 293, 295, 296ofval 6552 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T.  /\  x  e.  RR )  ->  (
( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x )  =  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
298286, 297mpan 675 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  ->  (
( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x )  =  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )
299298eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR  ->  ( -u 1  x.  if ( 0  <_  ( g `  x ) ,  ( g `  x ) ,  0 ) )  =  ( ( ( RR  X.  { -u
1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) )
300285, 299ifbieq1d 3933 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  RR  ->  if ( -.  x  e.  ( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  ( -u 1  x.  if ( 0  <_ 
( g `  x
) ,  ( g `
 x ) ,  0 ) ) ,  0 )  =  if ( x  e.  ( RR  \  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ) ,  ( ( ( RR  X.  { -u 1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) ,  0 ) )
301283, 300syl5eqr 2478 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  if ( x  e.  (
( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) )  =  if ( x  e.  ( RR  \  (
( `' ( Re  o.  F ) "
( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) ,  ( ( ( RR  X.  { -u 1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) ,  0 ) )
302301mpteq2ia 4504 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR  |->  if ( x  e.  ( ( `' ( Re  o.  F ) " (
0 [,) +oo )
)  u.  ( RR 
\  D ) ) ,  0 ,  (
-u 1  x.  if ( 0  <_  (
g `  x ) ,  ( g `  x ) ,  0 ) ) ) )  =  ( x  e.  RR  |->  if ( x  e.  ( RR  \ 
( ( `' ( Re  o.  F )
" ( 0 [,) +oo ) )  u.  ( RR  \  D ) ) ) ,  ( ( ( RR  X.  { -u 1 } )  oF  x.  ( t  e.  RR  |->  if ( 0  <_  ( g `  t ) ,  ( g `  t ) ,  0 ) ) ) `  x ) ,  0 ) )
303302i1fres 22655 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( RR  X.  { -u 1 } )  oF  x.  (
t  e.  RR  |->  if ( 0  <_  (
g `  t ) ,  ( g `  t ) ,  0 ) )