Step |
Hyp |
Ref |
Expression |
1 |
|
isibl.1 |
|- ( ph -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) |
2 |
|
isibl.2 |
|- ( ( ph /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ k ) ) ) ) |
3 |
|
isibl.3 |
|- ( ph -> dom F = A ) |
4 |
|
isibl.4 |
|- ( ( ph /\ x e. A ) -> ( F ` x ) = B ) |
5 |
|
fvex |
|- ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) e. _V |
6 |
|
breq2 |
|- ( y = ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) -> ( 0 <_ y <-> 0 <_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) ) ) |
7 |
6
|
anbi2d |
|- ( y = ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) -> ( ( x e. dom f /\ 0 <_ y ) <-> ( x e. dom f /\ 0 <_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) ) ) ) |
8 |
|
id |
|- ( y = ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) -> y = ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) ) |
9 |
7 8
|
ifbieq1d |
|- ( y = ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) -> if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) = if ( ( x e. dom f /\ 0 <_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) , 0 ) ) |
10 |
5 9
|
csbie |
|- [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) = if ( ( x e. dom f /\ 0 <_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) , 0 ) |
11 |
|
dmeq |
|- ( f = F -> dom f = dom F ) |
12 |
11
|
eleq2d |
|- ( f = F -> ( x e. dom f <-> x e. dom F ) ) |
13 |
|
fveq1 |
|- ( f = F -> ( f ` x ) = ( F ` x ) ) |
14 |
13
|
fvoveq1d |
|- ( f = F -> ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) = ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) |
15 |
14
|
breq2d |
|- ( f = F -> ( 0 <_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) ) |
16 |
12 15
|
anbi12d |
|- ( f = F -> ( ( x e. dom f /\ 0 <_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) ) <-> ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) ) ) |
17 |
16 14
|
ifbieq1d |
|- ( f = F -> if ( ( x e. dom f /\ 0 <_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) |
18 |
10 17
|
syl5eq |
|- ( f = F -> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) = if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) |
19 |
18
|
mpteq2dv |
|- ( f = F -> ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) = ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) |
20 |
19
|
fveq2d |
|- ( f = F -> ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) ) |
21 |
20
|
eleq1d |
|- ( f = F -> ( ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) |
22 |
21
|
ralbidv |
|- ( f = F -> ( A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR <-> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) |
23 |
|
df-ibl |
|- L^1 = { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR } |
24 |
22 23
|
elrab2 |
|- ( F e. L^1 <-> ( F e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) |
25 |
3
|
eleq2d |
|- ( ph -> ( x e. dom F <-> x e. A ) ) |
26 |
25
|
anbi1d |
|- ( ph -> ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) <-> ( x e. A /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) ) ) |
27 |
26
|
ifbid |
|- ( ph -> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) |
28 |
4
|
fvoveq1d |
|- ( ( ph /\ x e. A ) -> ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) ) |
29 |
28 2
|
eqtr4d |
|- ( ( ph /\ x e. A ) -> ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) = T ) |
30 |
29
|
ibllem |
|- ( ph -> if ( ( x e. A /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) |
31 |
27 30
|
eqtrd |
|- ( ph -> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) |
32 |
31
|
mpteq2dv |
|- ( ph -> ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) |
33 |
32 1
|
eqtr4d |
|- ( ph -> ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) = G ) |
34 |
33
|
fveq2d |
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` G ) ) |
35 |
34
|
eleq1d |
|- ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` G ) e. RR ) ) |
36 |
35
|
ralbidv |
|- ( ph -> ( A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> A. k e. ( 0 ... 3 ) ( S.2 ` G ) e. RR ) ) |
37 |
36
|
anbi2d |
|- ( ph -> ( ( F e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. dom F /\ 0 <_ ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( F ` x ) / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) <-> ( F e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` G ) e. RR ) ) ) |
38 |
24 37
|
syl5bb |
|- ( ph -> ( F e. L^1 <-> ( F e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` G ) e. RR ) ) ) |