Metamath Proof Explorer

Theorem fourierdlem110

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem110.a 
|- ( ph -> A e. RR )
fourierdlem110.b 
|- ( ph -> B e. RR )
fourierdlem110.t 
|- T = ( B - A )
fourierdlem110.x 
|- ( ph -> X e. RR )
fourierdlem110.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem110.m 
|- ( ph -> M e. NN )
fourierdlem110.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem110.f 
|- ( ph -> F : RR --> CC )
fourierdlem110.fper 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem110.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem110.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem110.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
Assertion fourierdlem110 
|- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

Step Hyp Ref Expression
1 fourierdlem110.a 
 |-  ( ph -> A e. RR )
2 fourierdlem110.b 
 |-  ( ph -> B e. RR )
3 fourierdlem110.t 
 |-  T = ( B - A )
4 fourierdlem110.x 
 |-  ( ph -> X e. RR )
5 fourierdlem110.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
6 fourierdlem110.m 
 |-  ( ph -> M e. NN )
7 fourierdlem110.q 
 |-  ( ph -> Q e. ( P ` M ) )
8 fourierdlem110.f 
 |-  ( ph -> F : RR --> CC )
9 fourierdlem110.fper 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
10 fourierdlem110.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem110.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
12 fourierdlem110.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
13 eqid 
 |-  ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
14 oveq1 
 |-  ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
15 14 eleq1d 
 |-  ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
16 15 rexbidv 
 |-  ( y = x -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
17 16 cbvrabv 
 |-  { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
18 17 uneq2i 
 |-  ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( A - X ) , ( B - X ) } u. { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
19 oveq1 
 |-  ( l = k -> ( l x. T ) = ( k x. T ) )
20 19 oveq2d 
 |-  ( l = k -> ( y + ( l x. T ) ) = ( y + ( k x. T ) ) )
21 20 eleq1d 
 |-  ( l = k -> ( ( y + ( l x. T ) ) e. ran Q <-> ( y + ( k x. T ) ) e. ran Q ) )
22 21 cbvrexvw 
 |-  ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. T ) ) e. ran Q )
23 22 a1i 
 |-  ( y e. ( ( A - X ) [,] ( B - X ) ) -> ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. T ) ) e. ran Q ) )
24 23 rabbiia 
 |-  { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } = { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q }
25 24 uneq2i 
 |-  ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
26 25 fveq2i 
 |-  ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) = ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
27 26 oveq1i 
 |-  ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
28 isoeq5 
 |-  ( ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
29 25 28 ax-mp 
 |-  ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
30 isoeq1 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
31 29 30 syl5bb 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
32 31 cbviotavw 
 |-  ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
33 id 
 |-  ( y = x -> y = x )
34 oveq2 
 |-  ( y = x -> ( B - y ) = ( B - x ) )
35 34 oveq1d 
 |-  ( y = x -> ( ( B - y ) / T ) = ( ( B - x ) / T ) )
36 35 fveq2d 
 |-  ( y = x -> ( |_ ` ( ( B - y ) / T ) ) = ( |_ ` ( ( B - x ) / T ) ) )
37 36 oveq1d 
 |-  ( y = x -> ( ( |_ ` ( ( B - y ) / T ) ) x. T ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
38 33 37 oveq12d 
 |-  ( y = x -> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
39 38 cbvmptv 
 |-  ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
40 eqeq1 
 |-  ( y = w -> ( y = B <-> w = B ) )
41 id 
 |-  ( y = w -> y = w )
42 40 41 ifbieq2d 
 |-  ( y = w -> if ( y = B , A , y ) = if ( w = B , A , w ) )
43 42 cbvmptv 
 |-  ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) = ( w e. ( A (,] B ) |-> if ( w = B , A , w ) )
44 fveq2 
 |-  ( z = x -> ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` z ) = ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` x ) )
45 44 fveq2d 
 |-  ( z = x -> ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` z ) ) = ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` x ) ) )
46 45 breq2d 
 |-  ( z = x -> ( ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` z ) ) <-> ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` x ) ) ) )
47 46 rabbidv 
 |-  ( z = x -> { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` z ) ) } = { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` x ) ) } )
48 47 supeq1d 
 |-  ( z = x -> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` z ) ) } , RR , < ) = sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
49 48 cbvmptv 
 |-  ( z e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` z ) ) } , RR , < ) ) = ( x e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) ` ( ( y e. RR |-> ( y + ( ( |_ ` ( ( B - y ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 13 18 27 32 39 43 49 fourierdlem109 
 |-  ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )