Metamath Proof Explorer

Theorem ftc1anclem6

Description: Lemma for ftc1anc - construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of Fremlin5 p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued F . (Contributed by Brendan Leahy, 31-May-2018)

Ref Expression
Hypotheses 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 ftc1anclem6 
|- ( ( ph /\ Y e. RR+ ) -> E. f e. dom S.1 E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < Y )

Proof

Step Hyp Ref Expression
1 ftc1anc.g 
 |-  G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2 ftc1anc.a 
 |-  ( ph -> A e. RR )
3 ftc1anc.b 
 |-  ( ph -> B e. RR )
4 ftc1anc.le 
 |-  ( ph -> A <_ B )
5 ftc1anc.s 
 |-  ( ph -> ( A (,) B ) C_ D )
6 ftc1anc.d 
 |-  ( ph -> D C_ RR )
7 ftc1anc.i 
 |-  ( ph -> F e. L^1 )
8 ftc1anc.f 
 |-  ( ph -> F : D --> CC )
9 rphalfcl 
 |-  ( Y e. RR+ -> ( Y / 2 ) e. RR+ )
10 1 2 3 4 5 6 7 8 ftc1anclem5 
 |-  ( ( ph /\ ( Y / 2 ) 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 / 2 ) )
11 9 10 sylan2 
 |-  ( ( 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 / 2 ) )
12 eqid 
 |-  ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) _d t ) = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) _d t )
13 ax-icn 
 |-  _i e. CC
14 ine0 
 |-  _i =/= 0
15 13 14 reccli 
 |-  ( 1 / _i ) e. CC
16 15 a1i 
 |-  ( ph -> ( 1 / _i ) e. CC )
17 8 ffvelrnda 
 |-  ( ( ph /\ y e. D ) -> ( F ` y ) e. CC )
18 8 feqmptd 
 |-  ( ph -> F = ( y e. D |-> ( F ` y ) ) )
19 18 7 eqeltrrd 
 |-  ( ph -> ( y e. D |-> ( F ` y ) ) e. L^1 )
20 divrec2 
 |-  ( ( ( F ` y ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( F ` y ) / _i ) = ( ( 1 / _i ) x. ( F ` y ) ) )
21 13 14 20 mp3an23 
 |-  ( ( F ` y ) e. CC -> ( ( F ` y ) / _i ) = ( ( 1 / _i ) x. ( F ` y ) ) )
22 17 21 syl 
 |-  ( ( ph /\ y e. D ) -> ( ( F ` y ) / _i ) = ( ( 1 / _i ) x. ( F ` y ) ) )
23 22 mpteq2dva 
 |-  ( ph -> ( y e. D |-> ( ( F ` y ) / _i ) ) = ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) )
24 iblmbf 
 |-  ( ( y e. D |-> ( F ` y ) ) e. L^1 -> ( y e. D |-> ( F ` y ) ) e. MblFn )
25 19 24 syl 
 |-  ( ph -> ( y e. D |-> ( F ` y ) ) e. MblFn )
26 2fveq3 
 |-  ( y = x -> ( Re ` ( F ` y ) ) = ( Re ` ( F ` x ) ) )
27 26 cbvmptv 
 |-  ( y e. D |-> ( Re ` ( F ` y ) ) ) = ( x e. D |-> ( Re ` ( F ` x ) ) )
28 27 eleq1i 
 |-  ( ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn <-> ( x e. D |-> ( Re ` ( F ` x ) ) ) e. MblFn )
29 17 recld 
 |-  ( ( ph /\ y e. D ) -> ( Re ` ( F ` y ) ) e. RR )
30 29 recnd 
 |-  ( ( ph /\ y e. D ) -> ( Re ` ( F ` y ) ) e. CC )
31 30 adantlr 
 |-  ( ( ( ph /\ ( x e. D |-> ( Re ` ( F ` x ) ) ) e. MblFn ) /\ y e. D ) -> ( Re ` ( F ` y ) ) e. CC )
32 28 biimpri 
 |-  ( ( x e. D |-> ( Re ` ( F ` x ) ) ) e. MblFn -> ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn )
33 32 adantl 
 |-  ( ( ph /\ ( x e. D |-> ( Re ` ( F ` x ) ) ) e. MblFn ) -> ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn )
34 31 33 mbfneg 
 |-  ( ( ph /\ ( x e. D |-> ( Re ` ( F ` x ) ) ) e. MblFn ) -> ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn )
35 28 34 sylan2b 
 |-  ( ( ph /\ ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn ) -> ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn )
36 8 ffvelrnda 
 |-  ( ( ph /\ x e. D ) -> ( F ` x ) e. CC )
37 36 recld 
 |-  ( ( ph /\ x e. D ) -> ( Re ` ( F ` x ) ) e. RR )
38 37 recnd 
 |-  ( ( ph /\ x e. D ) -> ( Re ` ( F ` x ) ) e. CC )
39 38 negnegd 
 |-  ( ( ph /\ x e. D ) -> -u -u ( Re ` ( F ` x ) ) = ( Re ` ( F ` x ) ) )
40 39 mpteq2dva 
 |-  ( ph -> ( x e. D |-> -u -u ( Re ` ( F ` x ) ) ) = ( x e. D |-> ( Re ` ( F ` x ) ) ) )
41 40 27 eqtr4di 
 |-  ( ph -> ( x e. D |-> -u -u ( Re ` ( F ` x ) ) ) = ( y e. D |-> ( Re ` ( F ` y ) ) ) )
42 41 adantr 
 |-  ( ( ph /\ ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn ) -> ( x e. D |-> -u -u ( Re ` ( F ` x ) ) ) = ( y e. D |-> ( Re ` ( F ` y ) ) ) )
43 negex 
 |-  -u ( Re ` ( F ` x ) ) e. _V
44 43 a1i 
 |-  ( ( ( ph /\ ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn ) /\ x e. D ) -> -u ( Re ` ( F ` x ) ) e. _V )
45 26 negeqd 
 |-  ( y = x -> -u ( Re ` ( F ` y ) ) = -u ( Re ` ( F ` x ) ) )
46 45 cbvmptv 
 |-  ( y e. D |-> -u ( Re ` ( F ` y ) ) ) = ( x e. D |-> -u ( Re ` ( F ` x ) ) )
47 46 eleq1i 
 |-  ( ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn <-> ( x e. D |-> -u ( Re ` ( F ` x ) ) ) e. MblFn )
48 47 biimpi 
 |-  ( ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn -> ( x e. D |-> -u ( Re ` ( F ` x ) ) ) e. MblFn )
49 48 adantl 
 |-  ( ( ph /\ ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn ) -> ( x e. D |-> -u ( Re ` ( F ` x ) ) ) e. MblFn )
50 44 49 mbfneg 
 |-  ( ( ph /\ ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn ) -> ( x e. D |-> -u -u ( Re ` ( F ` x ) ) ) e. MblFn )
51 42 50 eqeltrrd 
 |-  ( ( ph /\ ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn ) -> ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn )
52 35 51 impbida 
 |-  ( ph -> ( ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn <-> ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn ) )
53 divcl 
 |-  ( ( ( F ` y ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( F ` y ) / _i ) e. CC )
54 imre 
 |-  ( ( ( F ` y ) / _i ) e. CC -> ( Im ` ( ( F ` y ) / _i ) ) = ( Re ` ( -u _i x. ( ( F ` y ) / _i ) ) ) )
55 53 54 syl 
 |-  ( ( ( F ` y ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( Im ` ( ( F ` y ) / _i ) ) = ( Re ` ( -u _i x. ( ( F ` y ) / _i ) ) ) )
56 13 14 55 mp3an23 
 |-  ( ( F ` y ) e. CC -> ( Im ` ( ( F ` y ) / _i ) ) = ( Re ` ( -u _i x. ( ( F ` y ) / _i ) ) ) )
57 13 14 53 mp3an23 
 |-  ( ( F ` y ) e. CC -> ( ( F ` y ) / _i ) e. CC )
58 mulneg1 
 |-  ( ( _i e. CC /\ ( ( F ` y ) / _i ) e. CC ) -> ( -u _i x. ( ( F ` y ) / _i ) ) = -u ( _i x. ( ( F ` y ) / _i ) ) )
59 13 57 58 sylancr 
 |-  ( ( F ` y ) e. CC -> ( -u _i x. ( ( F ` y ) / _i ) ) = -u ( _i x. ( ( F ` y ) / _i ) ) )
60 divcan2 
 |-  ( ( ( F ` y ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( _i x. ( ( F ` y ) / _i ) ) = ( F ` y ) )
61 13 14 60 mp3an23 
 |-  ( ( F ` y ) e. CC -> ( _i x. ( ( F ` y ) / _i ) ) = ( F ` y ) )
62 61 negeqd 
 |-  ( ( F ` y ) e. CC -> -u ( _i x. ( ( F ` y ) / _i ) ) = -u ( F ` y ) )
63 59 62 eqtrd 
 |-  ( ( F ` y ) e. CC -> ( -u _i x. ( ( F ` y ) / _i ) ) = -u ( F ` y ) )
64 63 fveq2d 
 |-  ( ( F ` y ) e. CC -> ( Re ` ( -u _i x. ( ( F ` y ) / _i ) ) ) = ( Re ` -u ( F ` y ) ) )
65 reneg 
 |-  ( ( F ` y ) e. CC -> ( Re ` -u ( F ` y ) ) = -u ( Re ` ( F ` y ) ) )
66 56 64 65 3eqtrd 
 |-  ( ( F ` y ) e. CC -> ( Im ` ( ( F ` y ) / _i ) ) = -u ( Re ` ( F ` y ) ) )
67 17 66 syl 
 |-  ( ( ph /\ y e. D ) -> ( Im ` ( ( F ` y ) / _i ) ) = -u ( Re ` ( F ` y ) ) )
68 67 mpteq2dva 
 |-  ( ph -> ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) = ( y e. D |-> -u ( Re ` ( F ` y ) ) ) )
69 68 eleq1d 
 |-  ( ph -> ( ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) e. MblFn <-> ( y e. D |-> -u ( Re ` ( F ` y ) ) ) e. MblFn ) )
70 52 69 bitr4d 
 |-  ( ph -> ( ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn <-> ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) e. MblFn ) )
71 imval 
 |-  ( ( F ` y ) e. CC -> ( Im ` ( F ` y ) ) = ( Re ` ( ( F ` y ) / _i ) ) )
72 17 71 syl 
 |-  ( ( ph /\ y e. D ) -> ( Im ` ( F ` y ) ) = ( Re ` ( ( F ` y ) / _i ) ) )
73 72 mpteq2dva 
 |-  ( ph -> ( y e. D |-> ( Im ` ( F ` y ) ) ) = ( y e. D |-> ( Re ` ( ( F ` y ) / _i ) ) ) )
74 73 eleq1d 
 |-  ( ph -> ( ( y e. D |-> ( Im ` ( F ` y ) ) ) e. MblFn <-> ( y e. D |-> ( Re ` ( ( F ` y ) / _i ) ) ) e. MblFn ) )
75 70 74 anbi12d 
 |-  ( ph -> ( ( ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn /\ ( y e. D |-> ( Im ` ( F ` y ) ) ) e. MblFn ) <-> ( ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) e. MblFn /\ ( y e. D |-> ( Re ` ( ( F ` y ) / _i ) ) ) e. MblFn ) ) )
76 ancom 
 |-  ( ( ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) e. MblFn /\ ( y e. D |-> ( Re ` ( ( F ` y ) / _i ) ) ) e. MblFn ) <-> ( ( y e. D |-> ( Re ` ( ( F ` y ) / _i ) ) ) e. MblFn /\ ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) e. MblFn ) )
77 75 76 bitrdi 
 |-  ( ph -> ( ( ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn /\ ( y e. D |-> ( Im ` ( F ` y ) ) ) e. MblFn ) <-> ( ( y e. D |-> ( Re ` ( ( F ` y ) / _i ) ) ) e. MblFn /\ ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) e. MblFn ) ) )
78 17 ismbfcn2 
 |-  ( ph -> ( ( y e. D |-> ( F ` y ) ) e. MblFn <-> ( ( y e. D |-> ( Re ` ( F ` y ) ) ) e. MblFn /\ ( y e. D |-> ( Im ` ( F ` y ) ) ) e. MblFn ) ) )
79 17 57 syl 
 |-  ( ( ph /\ y e. D ) -> ( ( F ` y ) / _i ) e. CC )
80 79 ismbfcn2 
 |-  ( ph -> ( ( y e. D |-> ( ( F ` y ) / _i ) ) e. MblFn <-> ( ( y e. D |-> ( Re ` ( ( F ` y ) / _i ) ) ) e. MblFn /\ ( y e. D |-> ( Im ` ( ( F ` y ) / _i ) ) ) e. MblFn ) ) )
81 77 78 80 3bitr4d 
 |-  ( ph -> ( ( y e. D |-> ( F ` y ) ) e. MblFn <-> ( y e. D |-> ( ( F ` y ) / _i ) ) e. MblFn ) )
82 25 81 mpbid 
 |-  ( ph -> ( y e. D |-> ( ( F ` y ) / _i ) ) e. MblFn )
83 23 82 eqeltrrd 
 |-  ( ph -> ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) e. MblFn )
84 16 17 19 83 iblmulc2nc 
 |-  ( ph -> ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) e. L^1 )
85 mulcl 
 |-  ( ( ( 1 / _i ) e. CC /\ ( F ` y ) e. CC ) -> ( ( 1 / _i ) x. ( F ` y ) ) e. CC )
86 15 17 85 sylancr 
 |-  ( ( ph /\ y e. D ) -> ( ( 1 / _i ) x. ( F ` y ) ) e. CC )
87 86 fmpttd 
 |-  ( ph -> ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) : D --> CC )
88 12 2 3 4 5 6 84 87 ftc1anclem5 
 |-  ( ( ph /\ ( Y / 2 ) e. RR+ ) -> E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) )
89 9 88 sylan2 
 |-  ( ( ph /\ Y e. RR+ ) -> E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) )
90 8 ffvelrnda 
 |-  ( ( ph /\ t e. D ) -> ( F ` t ) e. CC )
91 0cnd 
 |-  ( ( ph /\ -. t e. D ) -> 0 e. CC )
92 90 91 ifclda 
 |-  ( ph -> if ( t e. D , ( F ` t ) , 0 ) e. CC )
93 imval 
 |-  ( if ( t e. D , ( F ` t ) , 0 ) e. CC -> ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) = ( Re ` ( if ( t e. D , ( F ` t ) , 0 ) / _i ) ) )
94 92 93 syl 
 |-  ( ph -> ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) = ( Re ` ( if ( t e. D , ( F ` t ) , 0 ) / _i ) ) )
95 fveq2 
 |-  ( y = t -> ( F ` y ) = ( F ` t ) )
96 95 oveq2d 
 |-  ( y = t -> ( ( 1 / _i ) x. ( F ` y ) ) = ( ( 1 / _i ) x. ( F ` t ) ) )
97 eqid 
 |-  ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) = ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) )
98 ovex 
 |-  ( ( 1 / _i ) x. ( F ` t ) ) e. _V
99 96 97 98 fvmpt 
 |-  ( t e. D -> ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) = ( ( 1 / _i ) x. ( F ` t ) ) )
100 99 adantl 
 |-  ( ( ph /\ t e. D ) -> ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) = ( ( 1 / _i ) x. ( F ` t ) ) )
101 divrec2 
 |-  ( ( ( F ` t ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( F ` t ) / _i ) = ( ( 1 / _i ) x. ( F ` t ) ) )
102 13 14 101 mp3an23 
 |-  ( ( F ` t ) e. CC -> ( ( F ` t ) / _i ) = ( ( 1 / _i ) x. ( F ` t ) ) )
103 90 102 syl 
 |-  ( ( ph /\ t e. D ) -> ( ( F ` t ) / _i ) = ( ( 1 / _i ) x. ( F ` t ) ) )
104 100 103 eqtr4d 
 |-  ( ( ph /\ t e. D ) -> ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) = ( ( F ` t ) / _i ) )
105 104 ifeq1da 
 |-  ( ph -> if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) = if ( t e. D , ( ( F ` t ) / _i ) , 0 ) )
106 ovif 
 |-  ( if ( t e. D , ( F ` t ) , 0 ) / _i ) = if ( t e. D , ( ( F ` t ) / _i ) , ( 0 / _i ) )
107 13 14 div0i 
 |-  ( 0 / _i ) = 0
108 ifeq2 
 |-  ( ( 0 / _i ) = 0 -> if ( t e. D , ( ( F ` t ) / _i ) , ( 0 / _i ) ) = if ( t e. D , ( ( F ` t ) / _i ) , 0 ) )
109 107 108 ax-mp 
 |-  if ( t e. D , ( ( F ` t ) / _i ) , ( 0 / _i ) ) = if ( t e. D , ( ( F ` t ) / _i ) , 0 )
110 106 109 eqtri 
 |-  ( if ( t e. D , ( F ` t ) , 0 ) / _i ) = if ( t e. D , ( ( F ` t ) / _i ) , 0 )
111 105 110 eqtr4di 
 |-  ( ph -> if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) = ( if ( t e. D , ( F ` t ) , 0 ) / _i ) )
112 111 fveq2d 
 |-  ( ph -> ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) = ( Re ` ( if ( t e. D , ( F ` t ) , 0 ) / _i ) ) )
113 94 112 eqtr4d 
 |-  ( ph -> ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) = ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) )
114 113 fvoveq1d 
 |-  ( ph -> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) )
115 114 mpteq2dv 
 |-  ( ph -> ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) ) )
116 115 fveq2d 
 |-  ( ph -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) )
117 116 breq1d 
 |-  ( ph -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) )
118 117 rexbidv 
 |-  ( ph -> ( E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) <-> E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) )
119 118 adantr 
 |-  ( ( ph /\ Y e. RR+ ) -> ( E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) <-> E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( ( y e. D |-> ( ( 1 / _i ) x. ( F ` y ) ) ) ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) )
120 89 119 mpbird 
 |-  ( ( ph /\ Y e. RR+ ) -> E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) )
121 reeanv 
 |-  ( E. f e. dom S.1 E. g e. dom S.1 ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) <-> ( E. f e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) )
122 eleq1w 
 |-  ( x = t -> ( x e. D <-> t e. D ) )
123 fveq2 
 |-  ( x = t -> ( F ` x ) = ( F ` t ) )
124 122 123 ifbieq1d 
 |-  ( x = t -> if ( x e. D , ( F ` x ) , 0 ) = if ( t e. D , ( F ` t ) , 0 ) )
125 124 fveq2d 
 |-  ( x = t -> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) = ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
126 eqid 
 |-  ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) = ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) )
127 fvex 
 |-  ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. _V
128 125 126 127 fvmpt 
 |-  ( t e. RR -> ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) = ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
129 128 fvoveq1d 
 |-  ( t e. RR -> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( f ` t ) ) ) = ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) )
130 129 mpteq2ia 
 |-  ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( f ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) )
131 130 fveq2i 
 |-  ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( f ` t ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) )
132 rembl 
 |-  RR e. dom vol
133 132 a1i 
 |-  ( ph -> RR e. dom vol )
134 0cnd 
 |-  ( ( ph /\ -. x e. D ) -> 0 e. CC )
135 36 134 ifclda 
 |-  ( ph -> if ( x e. D , ( F ` x ) , 0 ) e. CC )
136 135 adantr 
 |-  ( ( ph /\ x e. D ) -> if ( x e. D , ( F ` x ) , 0 ) e. CC )
137 eldifn 
 |-  ( x e. ( RR \ D ) -> -. x e. D )
138 137 adantl 
 |-  ( ( ph /\ x e. ( RR \ D ) ) -> -. x e. D )
139 138 iffalsed 
 |-  ( ( ph /\ x e. ( RR \ D ) ) -> if ( x e. D , ( F ` x ) , 0 ) = 0 )
140 8 feqmptd 
 |-  ( ph -> F = ( x e. D |-> ( F ` x ) ) )
141 iftrue 
 |-  ( x e. D -> if ( x e. D , ( F ` x ) , 0 ) = ( F ` x ) )
142 141 mpteq2ia 
 |-  ( x e. D |-> if ( x e. D , ( F ` x ) , 0 ) ) = ( x e. D |-> ( F ` x ) )
143 140 142 eqtr4di 
 |-  ( ph -> F = ( x e. D |-> if ( x e. D , ( F ` x ) , 0 ) ) )
144 143 7 eqeltrrd 
 |-  ( ph -> ( x e. D |-> if ( x e. D , ( F ` x ) , 0 ) ) e. L^1 )
145 6 133 136 139 144 iblss2 
 |-  ( ph -> ( x e. RR |-> if ( x e. D , ( F ` x ) , 0 ) ) e. L^1 )
146 135 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. D , ( F ` x ) , 0 ) e. CC )
147 146 iblcn 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. D , ( F ` x ) , 0 ) ) e. L^1 <-> ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 ) ) )
148 145 147 mpbid 
 |-  ( ph -> ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 ) )
149 148 simpld 
 |-  ( ph -> ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 )
150 146 recld 
 |-  ( ( ph /\ x e. RR ) -> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) e. RR )
151 150 fmpttd 
 |-  ( ph -> ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR )
152 149 151 jca 
 |-  ( ph -> ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) )
153 ftc1anclem4 
 |-  ( ( f e. dom S.1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( f ` t ) ) ) ) ) e. RR )
154 153 3expb 
 |-  ( ( f e. dom S.1 /\ ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( f ` t ) ) ) ) ) e. RR )
155 152 154 sylan2 
 |-  ( ( f e. dom S.1 /\ ph ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( f ` t ) ) ) ) ) e. RR )
156 155 ancoms 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Re ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( f ` t ) ) ) ) ) e. RR )
157 131 156 eqeltrrid 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) e. RR )
158 124 fveq2d 
 |-  ( x = t -> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) = ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) )
159 eqid 
 |-  ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) = ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) )
160 fvex 
 |-  ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) e. _V
161 158 159 160 fvmpt 
 |-  ( t e. RR -> ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) = ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) )
162 161 fvoveq1d 
 |-  ( t e. RR -> ( abs ` ( ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( g ` t ) ) ) = ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) )
163 162 mpteq2ia 
 |-  ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( g ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) )
164 163 fveq2i 
 |-  ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( g ` t ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) )
165 148 simprd 
 |-  ( ph -> ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 )
166 135 imcld 
 |-  ( ph -> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) e. RR )
167 166 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) e. RR )
168 167 fmpttd 
 |-  ( ph -> ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR )
169 165 168 jca 
 |-  ( ph -> ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) )
170 ftc1anclem4 
 |-  ( ( g e. dom S.1 /\ ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( g ` t ) ) ) ) ) e. RR )
171 170 3expb 
 |-  ( ( g e. dom S.1 /\ ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) e. L^1 /\ ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) : RR --> RR ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( g ` t ) ) ) ) ) e. RR )
172 169 171 sylan2 
 |-  ( ( g e. dom S.1 /\ ph ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( g ` t ) ) ) ) ) e. RR )
173 172 ancoms 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( x e. RR |-> ( Im ` if ( x e. D , ( F ` x ) , 0 ) ) ) ` t ) - ( g ` t ) ) ) ) ) e. RR )
174 164 173 eqeltrrid 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR )
175 157 174 anim12dan 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) e. RR /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR ) )
176 9 rpred 
 |-  ( Y e. RR+ -> ( Y / 2 ) e. RR )
177 176 176 jca 
 |-  ( Y e. RR+ -> ( ( Y / 2 ) e. RR /\ ( Y / 2 ) e. RR ) )
178 lt2add 
 |-  ( ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) e. RR /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR ) /\ ( ( Y / 2 ) e. RR /\ ( Y / 2 ) e. RR ) ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) )
179 175 177 178 syl2an 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ Y e. RR+ ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) )
180 179 an32s 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) )
181 92 recld 
 |-  ( ph -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
182 181 recnd 
 |-  ( ph -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC )
183 i1ff 
 |-  ( f e. dom S.1 -> f : RR --> RR )
184 183 ffvelrnda 
 |-  ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. RR )
185 184 recnd 
 |-  ( ( f e. dom S.1 /\ t e. RR ) -> ( f ` t ) e. CC )
186 subcl 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ ( f ` t ) e. CC ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. CC )
187 182 185 186 syl2an 
 |-  ( ( ph /\ ( f e. dom S.1 /\ t e. RR ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. CC )
188 187 anassrs 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ t e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. CC )
189 188 adantlrr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. CC )
190 92 imcld 
 |-  ( ph -> ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
191 190 recnd 
 |-  ( ph -> ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC )
192 i1ff 
 |-  ( g e. dom S.1 -> g : RR --> RR )
193 192 ffvelrnda 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. RR )
194 193 recnd 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> ( g ` t ) e. CC )
195 subcl 
 |-  ( ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ ( g ` t ) e. CC ) -> ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) e. CC )
196 191 194 195 syl2an 
 |-  ( ( ph /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) e. CC )
197 196 anassrs 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) e. CC )
198 mulcl 
 |-  ( ( _i e. CC /\ ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) e. CC ) -> ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. CC )
199 13 197 198 sylancr 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. CC )
200 199 adantlrl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. CC )
201 189 200 addcld 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) e. CC )
202 201 abscld 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR )
203 202 rexrd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR* )
204 201 absge0d 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> 0 <_ ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) )
205 elxrge0 
 |-  ( ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. ( 0 [,] +oo ) <-> ( ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR* /\ 0 <_ ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
206 203 204 205 sylanbrc 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. ( 0 [,] +oo ) )
207 206 fmpttd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) : RR --> ( 0 [,] +oo ) )
208 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
209 ge0addcl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
210 208 209 sselid 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
211 210 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,] +oo ) )
212 188 abscld 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) e. RR )
213 188 absge0d 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ t e. RR ) -> 0 <_ ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) )
214 elrege0 
 |-  ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) e. RR /\ 0 <_ ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) )
215 212 213 214 sylanbrc 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) e. ( 0 [,) +oo ) )
216 215 fmpttd 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) : RR --> ( 0 [,) +oo ) )
217 216 adantrr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) : RR --> ( 0 [,) +oo ) )
218 197 abscld 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. RR )
219 197 absge0d 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> 0 <_ ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) )
220 elrege0 
 |-  ( ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. RR /\ 0 <_ ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) )
221 218 219 220 sylanbrc 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. ( 0 [,) +oo ) )
222 221 fmpttd 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) : RR --> ( 0 [,) +oo ) )
223 222 adantrl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) : RR --> ( 0 [,) +oo ) )
224 reex 
 |-  RR e. _V
225 224 a1i 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> RR e. _V )
226 inidm 
 |-  ( RR i^i RR ) = RR
227 211 217 223 225 225 226 off 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) : RR --> ( 0 [,] +oo ) )
228 189 200 abstrid 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) <_ ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) + ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) )
229 228 ralrimiva 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> A. t e. RR ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) <_ ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) + ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) )
230 ovexd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) + ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. _V )
231 eqidd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) = ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
232 fvexd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) e. _V )
233 fvexd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) e. _V )
234 eqidd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) )
235 absmul 
 |-  ( ( _i e. CC /\ ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) e. CC ) -> ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( ( abs ` _i ) x. ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) )
236 13 197 235 sylancr 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( ( abs ` _i ) x. ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) )
237 absi 
 |-  ( abs ` _i ) = 1
238 237 oveq1i 
 |-  ( ( abs ` _i ) x. ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( 1 x. ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) )
239 218 recnd 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) e. CC )
240 239 mulid2d 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( 1 x. ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) )
241 238 240 syl5eq 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( ( abs ` _i ) x. ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) )
242 236 241 eqtr2d 
 |-  ( ( ( ph /\ g e. dom S.1 ) /\ t e. RR ) -> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) = ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) )
243 242 mpteq2dva 
 |-  ( ( ph /\ g e. dom S.1 ) -> ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) )
244 243 adantrl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) )
245 225 232 233 234 244 offval2 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) = ( t e. RR |-> ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) + ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
246 225 202 230 231 245 ofrfval2 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) oR <_ ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) <-> A. t e. RR ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) <_ ( ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) + ( abs ` ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
247 229 246 mpbird 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) oR <_ ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) )
248 itg2le 
 |-  ( ( ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) : RR --> ( 0 [,] +oo ) /\ ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) : RR --> ( 0 [,] +oo ) /\ ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) oR <_ ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) <_ ( S.2 ` ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
249 207 227 247 248 syl3anc 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) <_ ( S.2 ` ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
250 absf 
 |-  abs : CC --> RR
251 250 a1i 
 |-  ( ( ph /\ f e. dom S.1 ) -> abs : CC --> RR )
252 251 188 cofmpt 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( abs o. ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) )
253 resubcl 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( f ` t ) e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. RR )
254 181 184 253 syl2an 
 |-  ( ( ph /\ ( f e. dom S.1 /\ t e. RR ) ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. RR )
255 254 anassrs 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ t e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. RR )
256 255 fmpttd 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) : RR --> RR )
257 132 a1i 
 |-  ( ( ph /\ f e. dom S.1 ) -> RR e. dom vol )
258 iunin2 
 |-  U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i U_ y e. ran f ( `' f " { y } ) )
259 imaiun 
 |-  ( `' f " U_ y e. ran f { y } ) = U_ y e. ran f ( `' f " { y } )
260 iunid 
 |-  U_ y e. ran f { y } = ran f
261 260 imaeq2i 
 |-  ( `' f " U_ y e. ran f { y } ) = ( `' f " ran f )
262 259 261 eqtr3i 
 |-  U_ y e. ran f ( `' f " { y } ) = ( `' f " ran f )
263 262 ineq2i 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i U_ y e. ran f ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " ran f ) )
264 258 263 eqtri 
 |-  U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " ran f ) )
265 cnvimass 
 |-  ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) C_ dom ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) )
266 ovex 
 |-  ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. _V
267 eqid 
 |-  ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) = ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) )
268 266 267 dmmpti 
 |-  dom ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) = RR
269 265 268 sseqtri 
 |-  ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) C_ RR
270 cnvimarndm 
 |-  ( `' f " ran f ) = dom f
271 183 fdmd 
 |-  ( f e. dom S.1 -> dom f = RR )
272 270 271 syl5eq 
 |-  ( f e. dom S.1 -> ( `' f " ran f ) = RR )
273 269 272 sseqtrrid 
 |-  ( f e. dom S.1 -> ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) C_ ( `' f " ran f ) )
274 df-ss 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) C_ ( `' f " ran f ) <-> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " ran f ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) )
275 273 274 sylib 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " ran f ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) )
276 264 275 syl5eq 
 |-  ( f e. dom S.1 -> U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) )
277 276 ad2antlr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) )
278 183 frnd 
 |-  ( f e. dom S.1 -> ran f C_ RR )
279 278 ad2antlr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> ran f C_ RR )
280 279 sselda 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> y e. RR )
281 181 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
282 resubcl 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ y e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR )
283 181 282 sylan 
 |-  ( ( ph /\ y e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR )
284 283 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR )
285 281 284 2thd 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR ) )
286 ltaddsub 
 |-  ( ( x e. RR /\ y e. RR /\ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR ) -> ( ( x + y ) < ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <-> x < ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) ) )
287 181 286 syl3an3 
 |-  ( ( x e. RR /\ y e. RR /\ ph ) -> ( ( x + y ) < ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <-> x < ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) ) )
288 287 3comr 
 |-  ( ( ph /\ x e. RR /\ y e. RR ) -> ( ( x + y ) < ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <-> x < ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) ) )
289 288 3expa 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( x + y ) < ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) <-> x < ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) ) )
290 285 289 anbi12d 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( x + y ) < ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) <-> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR /\ x < ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) ) ) )
291 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
292 291 rexrd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR* )
293 292 adantll 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( x + y ) e. RR* )
294 elioopnf 
 |-  ( ( x + y ) e. RR* -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( x + y ) < ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
295 293 294 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( x + y ) < ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
296 rexr 
 |-  ( x e. RR -> x e. RR* )
297 296 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> x e. RR* )
298 elioopnf 
 |-  ( x e. RR* -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( x (,) +oo ) <-> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR /\ x < ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) ) ) )
299 297 298 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( x (,) +oo ) <-> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR /\ x < ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) ) ) )
300 290 295 299 3bitr4rd 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( x (,) +oo ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) ) )
301 oveq2 
 |-  ( ( f ` t ) = y -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) )
302 301 eleq1d 
 |-  ( ( f ` t ) = y -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( x (,) +oo ) ) )
303 302 bibi1d 
 |-  ( ( f ` t ) = y -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) ) <-> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( x (,) +oo ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) ) ) )
304 300 303 syl5ibrcom 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( f ` t ) = y -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) ) ) )
305 304 pm5.32rd 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) ) )
306 305 adantllr 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. RR ) -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) ) )
307 280 306 syldan 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) ) )
308 307 rabbidv 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) } = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) } )
309 183 feqmptd 
 |-  ( f e. dom S.1 -> f = ( t e. RR |-> ( f ` t ) ) )
310 309 cnveqd 
 |-  ( f e. dom S.1 -> `' f = `' ( t e. RR |-> ( f ` t ) ) )
311 310 imaeq1d 
 |-  ( f e. dom S.1 -> ( `' f " { y } ) = ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) )
312 311 ineq2d 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) )
313 267 mptpreima 
 |-  ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) }
314 vex 
 |-  y e. _V
315 eqid 
 |-  ( t e. RR |-> ( f ` t ) ) = ( t e. RR |-> ( f ` t ) )
316 315 mptiniseg 
 |-  ( y e. _V -> ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) = { t e. RR | ( f ` t ) = y } )
317 314 316 ax-mp 
 |-  ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) = { t e. RR | ( f ` t ) = y }
318 313 317 ineq12i 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = ( { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) } i^i { t e. RR | ( f ` t ) = y } )
319 inrab 
 |-  ( { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) } i^i { t e. RR | ( f ` t ) = y } ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) }
320 318 319 eqtri 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) }
321 312 320 eqtrdi 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) } )
322 321 ad3antlr 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( x (,) +oo ) /\ ( f ` t ) = y ) } )
323 311 ineq2d 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) )
324 eqid 
 |-  ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) = ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) )
325 324 mptpreima 
 |-  ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) = { t e. RR | ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) }
326 325 317 ineq12i 
 |-  ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = ( { t e. RR | ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) } i^i { t e. RR | ( f ` t ) = y } )
327 inrab 
 |-  ( { t e. RR | ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) } i^i { t e. RR | ( f ` t ) = y } ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) }
328 326 327 eqtri 
 |-  ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) }
329 323 328 eqtrdi 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) } )
330 329 ad3antlr 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( ( x + y ) (,) +oo ) /\ ( f ` t ) = y ) } )
331 308 322 330 3eqtr4d 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) )
332 331 iuneq2dv 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) i^i ( `' f " { y } ) ) = U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) )
333 277 332 eqtr3d 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) = U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) )
334 i1frn 
 |-  ( f e. dom S.1 -> ran f e. Fin )
335 334 adantl 
 |-  ( ( ph /\ f e. dom S.1 ) -> ran f e. Fin )
336 92 adantr 
 |-  ( ( ph /\ t e. D ) -> if ( t e. D , ( F ` t ) , 0 ) e. CC )
337 eldifn 
 |-  ( t e. ( RR \ D ) -> -. t e. D )
338 337 adantl 
 |-  ( ( ph /\ t e. ( RR \ D ) ) -> -. t e. D )
339 338 iffalsed 
 |-  ( ( ph /\ t e. ( RR \ D ) ) -> if ( t e. D , ( F ` t ) , 0 ) = 0 )
340 8 feqmptd 
 |-  ( ph -> F = ( t e. D |-> ( F ` t ) ) )
341 iftrue 
 |-  ( t e. D -> if ( t e. D , ( F ` t ) , 0 ) = ( F ` t ) )
342 341 mpteq2ia 
 |-  ( t e. D |-> if ( t e. D , ( F ` t ) , 0 ) ) = ( t e. D |-> ( F ` t ) )
343 340 342 eqtr4di 
 |-  ( ph -> F = ( t e. D |-> if ( t e. D , ( F ` t ) , 0 ) ) )
344 iblmbf 
 |-  ( F e. L^1 -> F e. MblFn )
345 7 344 syl 
 |-  ( ph -> F e. MblFn )
346 343 345 eqeltrrd 
 |-  ( ph -> ( t e. D |-> if ( t e. D , ( F ` t ) , 0 ) ) e. MblFn )
347 6 133 336 339 346 mbfss 
 |-  ( ph -> ( t e. RR |-> if ( t e. D , ( F ` t ) , 0 ) ) e. MblFn )
348 92 adantr 
 |-  ( ( ph /\ t e. RR ) -> if ( t e. D , ( F ` t ) , 0 ) e. CC )
349 348 ismbfcn2 
 |-  ( ph -> ( ( t e. RR |-> if ( t e. D , ( F ` t ) , 0 ) ) e. MblFn <-> ( ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn /\ ( t e. RR |-> ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn ) ) )
350 347 349 mpbid 
 |-  ( ph -> ( ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn /\ ( t e. RR |-> ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn ) )
351 350 simpld 
 |-  ( ph -> ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn )
352 181 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR )
353 352 fmpttd 
 |-  ( ph -> ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) : RR --> RR )
354 mbfima 
 |-  ( ( ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn /\ ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) : RR --> RR ) -> ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) e. dom vol )
355 351 353 354 syl2anc 
 |-  ( ph -> ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) e. dom vol )
356 i1fima 
 |-  ( f e. dom S.1 -> ( `' f " { y } ) e. dom vol )
357 inmbl 
 |-  ( ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) e. dom vol /\ ( `' f " { y } ) e. dom vol ) -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) e. dom vol )
358 355 356 357 syl2an 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) e. dom vol )
359 358 ralrimivw 
 |-  ( ( ph /\ f e. dom S.1 ) -> A. y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) e. dom vol )
360 finiunmbl 
 |-  ( ( ran f e. Fin /\ A. y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) e. dom vol ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) e. dom vol )
361 335 359 360 syl2anc 
 |-  ( ( ph /\ f e. dom S.1 ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) e. dom vol )
362 361 adantr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( ( x + y ) (,) +oo ) ) i^i ( `' f " { y } ) ) e. dom vol )
363 333 362 eqeltrd 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( x (,) +oo ) ) e. dom vol )
364 iunin2 
 |-  U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i U_ y e. ran f ( `' f " { y } ) )
365 262 ineq2i 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i U_ y e. ran f ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " ran f ) )
366 364 365 eqtri 
 |-  U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " ran f ) )
367 cnvimass 
 |-  ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) C_ dom ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) )
368 367 268 sseqtri 
 |-  ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) C_ RR
369 368 272 sseqtrrid 
 |-  ( f e. dom S.1 -> ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) C_ ( `' f " ran f ) )
370 df-ss 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) C_ ( `' f " ran f ) <-> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " ran f ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) )
371 369 370 sylib 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " ran f ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) )
372 366 371 syl5eq 
 |-  ( f e. dom S.1 -> U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) )
373 372 ad2antlr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) )
374 284 281 2thd 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR ) )
375 ltsubadd 
 |-  ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ y e. RR /\ x e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) < x <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < ( x + y ) ) )
376 181 375 syl3an1 
 |-  ( ( ph /\ y e. RR /\ x e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) < x <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < ( x + y ) ) )
377 376 3expa 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) < x <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < ( x + y ) ) )
378 377 an32s 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) < x <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < ( x + y ) ) )
379 374 378 anbi12d 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR /\ ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) < x ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < ( x + y ) ) ) )
380 elioomnf 
 |-  ( x e. RR* -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( -oo (,) x ) <-> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR /\ ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) < x ) ) )
381 297 380 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( -oo (,) x ) <-> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. RR /\ ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) < x ) ) )
382 elioomnf 
 |-  ( ( x + y ) e. RR* -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < ( x + y ) ) ) )
383 293 382 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. RR /\ ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) < ( x + y ) ) ) )
384 379 381 383 3bitr4d 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( -oo (,) x ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) ) )
385 301 eleq1d 
 |-  ( ( f ` t ) = y -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( -oo (,) x ) ) )
386 385 bibi1d 
 |-  ( ( f ` t ) = y -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) ) <-> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - y ) e. ( -oo (,) x ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) ) ) )
387 384 386 syl5ibrcom 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( f ` t ) = y -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) <-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) ) ) )
388 387 pm5.32rd 
 |-  ( ( ( ph /\ x e. RR ) /\ y e. RR ) -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) ) )
389 388 adantllr 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. RR ) -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) ) )
390 280 389 syldan 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) <-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) ) )
391 390 rabbidv 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) } = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) } )
392 311 ineq2d 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) )
393 267 mptpreima 
 |-  ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) }
394 393 317 ineq12i 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = ( { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) } i^i { t e. RR | ( f ` t ) = y } )
395 inrab 
 |-  ( { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) } i^i { t e. RR | ( f ` t ) = y } ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) }
396 394 395 eqtri 
 |-  ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) }
397 392 396 eqtrdi 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) } )
398 397 ad3antlr 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) e. ( -oo (,) x ) /\ ( f ` t ) = y ) } )
399 311 ineq2d 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) )
400 324 mptpreima 
 |-  ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) = { t e. RR | ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) }
401 400 317 ineq12i 
 |-  ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = ( { t e. RR | ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) } i^i { t e. RR | ( f ` t ) = y } )
402 inrab 
 |-  ( { t e. RR | ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) } i^i { t e. RR | ( f ` t ) = y } ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) }
403 401 402 eqtri 
 |-  ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' ( t e. RR |-> ( f ` t ) ) " { y } ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) }
404 399 403 eqtrdi 
 |-  ( f e. dom S.1 -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) } )
405 404 ad3antlr 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) = { t e. RR | ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. ( -oo (,) ( x + y ) ) /\ ( f ` t ) = y ) } )
406 391 398 405 3eqtr4d 
 |-  ( ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) /\ y e. ran f ) -> ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) )
407 406 iuneq2dv 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) i^i ( `' f " { y } ) ) = U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) )
408 373 407 eqtr3d 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) = U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) )
409 mbfima 
 |-  ( ( ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. MblFn /\ ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) : RR --> RR ) -> ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) e. dom vol )
410 351 353 409 syl2anc 
 |-  ( ph -> ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) e. dom vol )
411 inmbl 
 |-  ( ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) e. dom vol /\ ( `' f " { y } ) e. dom vol ) -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) e. dom vol )
412 410 356 411 syl2an 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) e. dom vol )
413 412 ralrimivw 
 |-  ( ( ph /\ f e. dom S.1 ) -> A. y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) e. dom vol )
414 finiunmbl 
 |-  ( ( ran f e. Fin /\ A. y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) e. dom vol ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) e. dom vol )
415 335 413 414 syl2anc 
 |-  ( ( ph /\ f e. dom S.1 ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) e. dom vol )
416 415 adantr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> U_ y e. ran f ( ( `' ( t e. RR |-> ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) ) " ( -oo (,) ( x + y ) ) ) i^i ( `' f " { y } ) ) e. dom vol )
417 408 416 eqeltrd 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> ( `' ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) " ( -oo (,) x ) ) e. dom vol )
418 256 257 363 417 ismbf2d 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) e. MblFn )
419 ftc1anclem1 
 |-  ( ( ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) : RR --> RR /\ ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) e. MblFn ) -> ( abs o. ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) e. MblFn )
420 256 418 419 syl2anc 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( abs o. ( t e. RR |-> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) e. MblFn )
421 252 420 eqeltrrd 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) e. MblFn )
422 421 adantrr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) e. MblFn )
423 157 adantrr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) e. RR )
424 174 adantrl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR )
425 422 217 423 223 424 itg2addnc 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) oF + ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) = ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
426 249 425 breqtrd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
427 426 adantlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) )
428 itg2cl 
 |-  ( ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) e. RR* )
429 207 428 syl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) e. RR* )
430 429 adantlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) e. RR* )
431 readdcl 
 |-  ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) e. RR /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) e. RR ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) e. RR )
432 157 174 431 syl2an 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ ( ph /\ g e. dom S.1 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) e. RR )
433 432 anandis 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) e. RR )
434 433 rexrd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) e. RR* )
435 434 adantlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) e. RR* )
436 9 9 rpaddcld 
 |-  ( Y e. RR+ -> ( ( Y / 2 ) + ( Y / 2 ) ) e. RR+ )
437 436 rpxrd 
 |-  ( Y e. RR+ -> ( ( Y / 2 ) + ( Y / 2 ) ) e. RR* )
438 437 ad2antlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( Y / 2 ) + ( Y / 2 ) ) e. RR* )
439 xrlelttr 
 |-  ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) e. RR* /\ ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) e. RR* /\ ( ( Y / 2 ) + ( Y / 2 ) ) e. RR* ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) /\ ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) )
440 430 435 438 439 syl3anc 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) <_ ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) /\ ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) )
441 427 440 mpand 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) )
442 180 441 syld 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) ) )
443 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC ) -> ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. CC )
444 13 191 443 sylancr 
 |-  ( ph -> ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. CC )
445 182 444 jca 
 |-  ( ph -> ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. CC ) )
446 mulcl 
 |-  ( ( _i e. CC /\ ( g ` t ) e. CC ) -> ( _i x. ( g ` t ) ) e. CC )
447 13 194 446 sylancr 
 |-  ( ( g e. dom S.1 /\ t e. RR ) -> ( _i x. ( g ` t ) ) e. CC )
448 185 447 anim12i 
 |-  ( ( ( f e. dom S.1 /\ t e. RR ) /\ ( g e. dom S.1 /\ t e. RR ) ) -> ( ( f ` t ) e. CC /\ ( _i x. ( g ` t ) ) e. CC ) )
449 448 anandirs 
 |-  ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) -> ( ( f ` t ) e. CC /\ ( _i x. ( g ` t ) ) e. CC ) )
450 addsub4 
 |-  ( ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) e. CC ) /\ ( ( f ` t ) e. CC /\ ( _i x. ( g ` t ) ) e. CC ) ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) = ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) - ( _i x. ( g ` t ) ) ) ) )
451 445 449 450 syl2an 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) = ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) - ( _i x. ( g ` t ) ) ) ) )
452 451 anassrs 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) = ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) - ( _i x. ( g ` t ) ) ) ) )
453 92 replimd 
 |-  ( ph -> if ( t e. D , ( F ` t ) , 0 ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
454 453 ad2antrr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> if ( t e. D , ( F ` t ) , 0 ) = ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) )
455 454 oveq1d 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) = ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) + ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
456 194 adantll 
 |-  ( ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) -> ( g ` t ) e. CC )
457 subdi 
 |-  ( ( _i e. CC /\ ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) e. CC /\ ( g ` t ) e. CC ) -> ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) = ( ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) - ( _i x. ( g ` t ) ) ) )
458 13 191 456 457 mp3an3an 
 |-  ( ( ph /\ ( ( f e. dom S.1 /\ g e. dom S.1 ) /\ t e. RR ) ) -> ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) = ( ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) - ( _i x. ( g ` t ) ) ) )
459 458 anassrs 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) = ( ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) - ( _i x. ( g ` t ) ) ) )
460 459 oveq2d 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( ( _i x. ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) ) - ( _i x. ( g ` t ) ) ) ) )
461 452 455 460 3eqtr4rd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) = ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) )
462 461 fveq2d 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) /\ t e. RR ) -> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) = ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) )
463 462 mpteq2dva 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) = ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) )
464 463 fveq2d 
 |-  ( ( ph /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) )
465 464 adantlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) )
466 rpcn 
 |-  ( Y e. RR+ -> Y e. CC )
467 466 2halvesd 
 |-  ( Y e. RR+ -> ( ( Y / 2 ) + ( Y / 2 ) ) = Y )
468 467 ad2antlr 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( Y / 2 ) + ( Y / 2 ) ) = Y )
469 465 468 breq12d 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) + ( _i x. ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) ) ) < ( ( Y / 2 ) + ( Y / 2 ) ) <-> ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < Y ) )
470 442 469 sylibd 
 |-  ( ( ( ph /\ Y e. RR+ ) /\ ( f e. dom S.1 /\ g e. dom S.1 ) ) -> ( ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < Y ) )
471 470 reximdvva 
 |-  ( ( ph /\ Y e. RR+ ) -> ( E. f e. dom S.1 E. g e. dom S.1 ( ( S.2 ` ( t e. RR |-> ( abs ` ( ( Re ` if ( t e. D , ( F ` t ) , 0 ) ) - ( f ` t ) ) ) ) ) < ( Y / 2 ) /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) -> E. f e. dom S.1 E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < Y ) )
472 121 471 syl5bir 
 |-  ( ( 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 / 2 ) /\ E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( ( Im ` if ( t e. D , ( F ` t ) , 0 ) ) - ( g ` t ) ) ) ) ) < ( Y / 2 ) ) -> E. f e. dom S.1 E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < Y ) )
473 11 120 472 mp2and 
 |-  ( ( ph /\ Y e. RR+ ) -> E. f e. dom S.1 E. g e. dom S.1 ( S.2 ` ( t e. RR |-> ( abs ` ( if ( t e. D , ( F ` t ) , 0 ) - ( ( f ` t ) + ( _i x. ( g ` t ) ) ) ) ) ) ) < Y )