Metamath Proof Explorer

Theorem iblitg

Description: If a function is integrable, then the S.2 integrals of the function's decompositions all exist. (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 iblitg.1 
 |-  ( ph -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )
2 iblitg.2 
 |-  ( ( ph /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ K ) ) ) )
3 iblitg.3 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
4 iblitg.4 
 |-  ( ( ph /\ x e. A ) -> B e. V )
5 1 adantr 
 |-  ( ( ph /\ K e. ZZ ) -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )
6 2 adantlr 
 |-  ( ( ( ph /\ K e. ZZ ) /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ K ) ) ) )
7 iexpcyc 
 |-  ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )
8 7 oveq2d 
 |-  ( K e. ZZ -> ( B / ( _i ^ ( K mod 4 ) ) ) = ( B / ( _i ^ K ) ) )
9 8 fveq2d 
 |-  ( K e. ZZ -> ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) = ( Re ` ( B / ( _i ^ K ) ) ) )
10 9 ad2antlr 
 |-  ( ( ( ph /\ K e. ZZ ) /\ x e. A ) -> ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) = ( Re ` ( B / ( _i ^ K ) ) ) )
11 6 10 eqtr4d 
 |-  ( ( ( ph /\ K e. ZZ ) /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) )
12 11 ibllem 
 |-  ( ( ph /\ K e. ZZ ) -> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) )
13 12 mpteq2dv 
 |-  ( ( ph /\ K e. ZZ ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) )
14 5 13 eqtrd 
 |-  ( ( ph /\ K e. ZZ ) -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) )
15 14 fveq2d 
 |-  ( ( ph /\ K e. ZZ ) -> ( S.2 ` G ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) )
16 oveq2 
 |-  ( k = ( K mod 4 ) -> ( _i ^ k ) = ( _i ^ ( K mod 4 ) ) )
17 16 oveq2d 
 |-  ( k = ( K mod 4 ) -> ( B / ( _i ^ k ) ) = ( B / ( _i ^ ( K mod 4 ) ) ) )
18 17 fveq2d 
 |-  ( k = ( K mod 4 ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) )
19 18 breq2d 
 |-  ( k = ( K mod 4 ) -> ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) )
20 19 anbi2d 
 |-  ( k = ( K mod 4 ) -> ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) <-> ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) ) )
21 20 18 ifbieq1d 
 |-  ( k = ( K mod 4 ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) )
22 21 mpteq2dv 
 |-  ( k = ( K mod 4 ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) )
23 22 fveq2d 
 |-  ( k = ( K mod 4 ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) )
24 23 eleq1d 
 |-  ( k = ( K mod 4 ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) e. RR ) )
25 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
26 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) )
27 25 26 4 isibl2 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
28 3 27 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) )
29 28 simprd 
 |-  ( ph -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
30 29 adantr 
 |-  ( ( ph /\ K e. ZZ ) -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
31 4nn 
 |-  4 e. NN
32 zmodfz 
 |-  ( ( K e. ZZ /\ 4 e. NN ) -> ( K mod 4 ) e. ( 0 ... ( 4 - 1 ) ) )
33 31 32 mpan2 
 |-  ( K e. ZZ -> ( K mod 4 ) e. ( 0 ... ( 4 - 1 ) ) )
34 4m1e3 
 |-  ( 4 - 1 ) = 3
35 34 oveq2i 
 |-  ( 0 ... ( 4 - 1 ) ) = ( 0 ... 3 )
36 33 35 eleqtrdi 
 |-  ( K e. ZZ -> ( K mod 4 ) e. ( 0 ... 3 ) )
37 36 adantl 
 |-  ( ( ph /\ K e. ZZ ) -> ( K mod 4 ) e. ( 0 ... 3 ) )
38 24 30 37 rspcdva 
 |-  ( ( ph /\ K e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) e. RR )
39 15 38 eqeltrd 
 |-  ( ( ph /\ K e. ZZ ) -> ( S.2 ` G ) e. RR )