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