Metamath Proof Explorer

Theorem isibl

Description: The predicate " F is integrable". The "integrable" predicate corresponds roughly to the range of validity of S. A Bd x , which is to say that the expression S. A B d x doesn't make sense unless ( x e. A |-> B ) e. L^1 . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses isibl.1 
|- ( ph -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )
isibl.2 
|- ( ( ph /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ k ) ) ) )
isibl.3 
|- ( ph -> dom F = A )
isibl.4 
|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
Assertion isibl 
|- ( ph -> ( F e. L^1 <-> ( F e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` G ) e. RR ) ) )

Proof

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 ) ) )