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