Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem106.f |
|- ( ph -> F : RR --> RR ) |
2 |
|
fourierdlem106.t |
|- T = ( 2 x. _pi ) |
3 |
|
fourierdlem106.per |
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) |
4 |
|
fourierdlem106.g |
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |
5 |
|
fourierdlem106.dmdv |
|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin ) |
6 |
|
fourierdlem106.dvcn |
|- ( ph -> G e. ( dom G -cn-> CC ) ) |
7 |
|
fourierdlem106.rlim |
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) ) |
8 |
|
fourierdlem106.llim |
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) ) |
9 |
|
fourierdlem106.x |
|- ( ph -> X e. RR ) |
10 |
|
eqid |
|- ( k e. NN |-> { w e. ( RR ^m ( 0 ... k ) ) | ( ( ( w ` 0 ) = -u _pi /\ ( w ` k ) = _pi ) /\ A. z e. ( 0 ..^ k ) ( w ` z ) < ( w ` ( z + 1 ) ) ) } ) = ( k e. NN |-> { w e. ( RR ^m ( 0 ... k ) ) | ( ( ( w ` 0 ) = -u _pi /\ ( w ` k ) = _pi ) /\ A. z e. ( 0 ..^ k ) ( w ` z ) < ( w ` ( z + 1 ) ) ) } ) |
11 |
|
id |
|- ( y = x -> y = x ) |
12 |
|
oveq2 |
|- ( y = x -> ( _pi - y ) = ( _pi - x ) ) |
13 |
12
|
oveq1d |
|- ( y = x -> ( ( _pi - y ) / T ) = ( ( _pi - x ) / T ) ) |
14 |
13
|
fveq2d |
|- ( y = x -> ( |_ ` ( ( _pi - y ) / T ) ) = ( |_ ` ( ( _pi - x ) / T ) ) ) |
15 |
14
|
oveq1d |
|- ( y = x -> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) = ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) |
16 |
11 15
|
oveq12d |
|- ( y = x -> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) ) |
17 |
16
|
cbvmptv |
|- ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) ) |
18 |
|
eqid |
|- ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) = ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) |
19 |
|
eqid |
|- ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) = ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) |
20 |
|
isoeq1 |
|- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) ) ) |
21 |
20
|
cbviotavw |
|- ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) ) |
22 |
1 2 3 4 5 6 7 8 9 10 17 18 19 21
|
fourierdlem102 |
|- ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) ) |