Metamath Proof Explorer

Theorem isibl2

Description: The predicate " F is integrable" when F is a mapping operation. (Contributed by Mario Carneiro, 31-Jul-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 ) ) ) )
isibl2.3 
|- ( ( ph /\ x e. A ) -> B e. V )
Assertion isibl2 
|- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) 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 isibl2.3 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 nfv 
 |-  F/ x y e. A
5 nfcv 
 |-  F/_ x 0
6 nfcv 
 |-  F/_ x <_
7 nfcv 
 |-  F/_ x Re
8 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> B ) ` y )
9 nfcv 
 |-  F/_ x /
10 nfcv 
 |-  F/_ x ( _i ^ k )
11 8 9 10 nfov 
 |-  F/_ x ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) )
12 7 11 nffv 
 |-  F/_ x ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) )
13 5 6 12 nfbr 
 |-  F/ x 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) )
14 4 13 nfan 
 |-  F/ x ( y e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) )
15 14 12 5 nfif 
 |-  F/_ x if ( ( y e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) , 0 )
16 nfcv 
 |-  F/_ y if ( ( x e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) , 0 )
17 eleq1w 
 |-  ( y = x -> ( y e. A <-> x e. A ) )
18 fveq2 
 |-  ( y = x -> ( ( x e. A |-> B ) ` y ) = ( ( x e. A |-> B ) ` x ) )
19 18 fvoveq1d 
 |-  ( y = x -> ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) = ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) )
20 19 breq2d 
 |-  ( y = x -> ( 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) ) )
21 17 20 anbi12d 
 |-  ( y = x -> ( ( y e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) ) <-> ( x e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) ) ) )
22 21 19 ifbieq1d 
 |-  ( y = x -> if ( ( y e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) , 0 ) )
23 15 16 22 cbvmpt 
 |-  ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) , 0 ) )
24 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
25 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
26 25 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
27 24 3 26 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
28 27 fvoveq1d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) )
29 28 2 eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) = T )
30 29 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ T ) , T , 0 ) )
31 30 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` x ) / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )
32 23 31 eqtrid 
 |-  ( ph -> ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )
33 1 32 eqtr4d 
 |-  ( ph -> G = ( y e. RR |-> if ( ( y e. A /\ 0 <_ ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) ) , ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) , 0 ) ) )
34 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) = ( Re ` ( ( ( x e. A |-> B ) ` y ) / ( _i ^ k ) ) ) )
35 25 3 dmmptd 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
36 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( ( x e. A |-> B ) ` y ) = ( ( x e. A |-> B ) ` y ) )
37 33 34 35 36 isibl 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` G ) e. RR ) ) )