Metamath Proof Explorer

Theorem fourierdlem105

Description: A piecewise continuous function is integrable on any closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem105.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 ) ) ) } )
fourierdlem105.t 
|- T = ( B - A )
fourierdlem105.m 
|- ( ph -> M e. NN )
fourierdlem105.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem105.f 
|- ( ph -> F : RR --> CC )
fourierdlem105.6 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem105.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem105.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem105.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem105.c 
|- ( ph -> C e. RR )
fourierdlem105.d 
|- ( ph -> D e. ( C (,) +oo ) )
Assertion fourierdlem105 
|- ( ph -> ( x e. ( C [,] D ) |-> ( F ` x ) ) e. L^1 )

Proof

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