Metamath Proof Explorer


Theorem fourierdlem97

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem97.f
|- ( ph -> F : RR --> RR )
fourierdlem97.g
|- G = ( RR _D F )
fourierdlem97.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 ) ) ) } )
fourierdlem97.a
|- ( ph -> B e. RR )
fourierdlem97.b
|- ( ph -> A e. RR )
fourierdlem97.t
|- T = ( B - A )
fourierdlem97.m
|- ( ph -> M e. NN )
fourierdlem97.q
|- ( ph -> Q e. ( P ` M ) )
fourierdlem97.fper
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem97.qcn
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem97.c
|- ( ph -> C e. RR )
fourierdlem97.d
|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem97.j
|- ( ph -> J e. ( 0 ..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
fourierdlem97.v
|- V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
fourierdlem97.h
|- H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) )
Assertion fourierdlem97
|- ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fourierdlem97.f
 |-  ( ph -> F : RR --> RR )
2 fourierdlem97.g
 |-  G = ( RR _D F )
3 fourierdlem97.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 ) ) ) } )
4 fourierdlem97.a
 |-  ( ph -> B e. RR )
5 fourierdlem97.b
 |-  ( ph -> A e. RR )
6 fourierdlem97.t
 |-  T = ( B - A )
7 fourierdlem97.m
 |-  ( ph -> M e. NN )
8 fourierdlem97.q
 |-  ( ph -> Q e. ( P ` M ) )
9 fourierdlem97.fper
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
10 fourierdlem97.qcn
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem97.c
 |-  ( ph -> C e. RR )
12 fourierdlem97.d
 |-  ( ph -> D e. ( C (,) +oo ) )
13 fourierdlem97.j
 |-  ( ph -> J e. ( 0 ..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
14 fourierdlem97.v
 |-  V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
15 fourierdlem97.h
 |-  H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) )
16 ioossre
 |-  ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ RR
17 16 a1i
 |-  ( ph -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ RR )
18 17 sselda
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> s e. RR )
19 iftrue
 |-  ( s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
20 19 adantl
 |-  ( ( ph /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
21 ssid
 |-  RR C_ RR
22 dvfre
 |-  ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
23 1 21 22 sylancl
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
24 2 feq1i
 |-  ( G : dom ( RR _D F ) --> RR <-> ( RR _D F ) : dom ( RR _D F ) --> RR )
25 23 24 sylibr
 |-  ( ph -> G : dom ( RR _D F ) --> RR )
26 25 adantr
 |-  ( ( ph /\ s e. dom G ) -> G : dom ( RR _D F ) --> RR )
27 id
 |-  ( s e. dom G -> s e. dom G )
28 2 dmeqi
 |-  dom G = dom ( RR _D F )
29 27 28 eleqtrdi
 |-  ( s e. dom G -> s e. dom ( RR _D F ) )
30 29 adantl
 |-  ( ( ph /\ s e. dom G ) -> s e. dom ( RR _D F ) )
31 26 30 ffvelrnd
 |-  ( ( ph /\ s e. dom G ) -> ( G ` s ) e. RR )
32 20 31 eqeltrd
 |-  ( ( ph /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
33 32 adantlr
 |-  ( ( ( ph /\ s e. RR ) /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
34 iffalse
 |-  ( -. s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) = 0 )
35 0red
 |-  ( -. s e. dom G -> 0 e. RR )
36 34 35 eqeltrd
 |-  ( -. s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
37 36 adantl
 |-  ( ( ( ph /\ s e. RR ) /\ -. s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
38 33 37 pm2.61dan
 |-  ( ( ph /\ s e. RR ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
39 18 38 syldan
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
40 15 fvmpt2
 |-  ( ( s e. RR /\ if ( s e. dom G , ( G ` s ) , 0 ) e. RR ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
41 18 39 40 syl2anc
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
42 elioore
 |-  ( D e. ( C (,) +oo ) -> D e. RR )
43 12 42 syl
 |-  ( ph -> D e. RR )
44 11 rexrd
 |-  ( ph -> C e. RR* )
45 pnfxr
 |-  +oo e. RR*
46 45 a1i
 |-  ( ph -> +oo e. RR* )
47 ioogtlb
 |-  ( ( C e. RR* /\ +oo e. RR* /\ D e. ( C (,) +oo ) ) -> C < D )
48 44 46 12 47 syl3anc
 |-  ( ph -> C < D )
49 oveq1
 |-  ( y = x -> ( y + ( h x. T ) ) = ( x + ( h x. T ) ) )
50 49 eleq1d
 |-  ( y = x -> ( ( y + ( h x. T ) ) e. ran Q <-> ( x + ( h x. T ) ) e. ran Q ) )
51 50 rexbidv
 |-  ( y = x -> ( E. h e. ZZ ( y + ( h x. T ) ) e. ran Q <-> E. h e. ZZ ( x + ( h x. T ) ) e. ran Q ) )
52 51 cbvrabv
 |-  { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } = { x e. ( C [,] D ) | E. h e. ZZ ( x + ( h x. T ) ) e. ran Q }
53 52 uneq2i
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) | E. h e. ZZ ( x + ( h x. T ) ) e. ran Q } )
54 oveq1
 |-  ( k = l -> ( k x. T ) = ( l x. T ) )
55 54 oveq2d
 |-  ( k = l -> ( y + ( k x. T ) ) = ( y + ( l x. T ) ) )
56 55 eleq1d
 |-  ( k = l -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
57 56 cbvrexvw
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q )
58 57 a1i
 |-  ( y e. ( C [,] D ) -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) )
59 58 rabbiia
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q }
60 59 uneq2i
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } )
61 oveq1
 |-  ( l = h -> ( l x. T ) = ( h x. T ) )
62 61 oveq2d
 |-  ( l = h -> ( y + ( l x. T ) ) = ( y + ( h x. T ) ) )
63 62 eleq1d
 |-  ( l = h -> ( ( y + ( l x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
64 63 cbvrexvw
 |-  ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
65 64 a1i
 |-  ( y e. ( C [,] D ) -> ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q ) )
66 65 rabbiia
 |-  { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q }
67 66 uneq2i
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
68 60 67 eqtri
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
69 68 fveq2i
 |-  ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) )
70 69 oveq1i
 |-  ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) - 1 )
71 oveq1
 |-  ( k = h -> ( k x. T ) = ( h x. T ) )
72 71 oveq2d
 |-  ( k = h -> ( ( Q ` 0 ) + ( k x. T ) ) = ( ( Q ` 0 ) + ( h x. T ) ) )
73 72 breq1d
 |-  ( k = h -> ( ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) <-> ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) ) )
74 73 cbvrabv
 |-  { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } = { h e. ZZ | ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) }
75 74 supeq1i
 |-  sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) = sup ( { h e. ZZ | ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) } , RR , < )
76 fveq2
 |-  ( j = e -> ( Q ` j ) = ( Q ` e ) )
77 76 oveq1d
 |-  ( j = e -> ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) = ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) )
78 77 breq1d
 |-  ( j = e -> ( ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) <-> ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) ) )
79 78 cbvrabv
 |-  { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } = { e e. ( 0 ..^ M ) | ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) }
80 79 supeq1i
 |-  sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < ) = sup ( { e e. ( 0 ..^ M ) | ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < )
81 6 3 7 8 11 43 48 53 70 14 13 75 80 fourierdlem64
 |-  ( ph -> ( ( sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < ) e. ( 0 ..^ M ) /\ sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) e. ZZ ) /\ E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) )
82 81 simprd
 |-  ( ph -> E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
83 simpl1
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ph )
84 simpl2l
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
85 cncff
 |-  ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
86 10 85 syl
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
87 ffun
 |-  ( G : dom ( RR _D F ) --> RR -> Fun G )
88 25 87 syl
 |-  ( ph -> Fun G )
89 88 adantr
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Fun G )
90 ffvresb
 |-  ( Fun G -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) ) )
91 89 90 syl
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) ) )
92 86 91 mpbid
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) )
93 92 r19.21bi
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. dom G /\ ( G ` s ) e. CC ) )
94 93 simpld
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. dom G )
95 94 ralrimiva
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) s e. dom G )
96 dfss3
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) s e. dom G )
97 95 96 sylibr
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
98 83 84 97 syl2anc
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
99 simpl2
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( i e. ( 0 ..^ M ) /\ l e. ZZ ) )
100 83 99 jca
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) )
101 simpl3
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
102 simpr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) )
103 101 102 sseldd
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
104 3 fourierdlem2
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
105 7 104 syl
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
106 8 105 mpbid
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
107 106 simpld
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
108 elmapi
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
109 107 108 syl
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
110 109 adantr
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
111 elfzofz
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
112 111 adantl
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
113 110 112 ffvelrnd
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
114 113 rexrd
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
115 114 adantrr
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( Q ` i ) e. RR* )
116 115 adantr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) e. RR* )
117 fzofzp1
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
118 117 adantl
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
119 110 118 ffvelrnd
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
120 119 adantrr
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( Q ` ( i + 1 ) ) e. RR )
121 120 adantr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
122 121 rexrd
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
123 elioore
 |-  ( t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> t e. RR )
124 123 adantl
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. RR )
125 zre
 |-  ( l e. ZZ -> l e. RR )
126 125 adantl
 |-  ( ( i e. ( 0 ..^ M ) /\ l e. ZZ ) -> l e. RR )
127 126 ad2antlr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> l e. RR )
128 4 5 resubcld
 |-  ( ph -> ( B - A ) e. RR )
129 6 128 eqeltrid
 |-  ( ph -> T e. RR )
130 129 ad2antrr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> T e. RR )
131 127 130 remulcld
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( l x. T ) e. RR )
132 124 131 resubcld
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) e. RR )
133 113 adantrr
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( Q ` i ) e. RR )
134 125 ad2antll
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> l e. RR )
135 129 adantr
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> T e. RR )
136 134 135 remulcld
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( l x. T ) e. RR )
137 133 136 readdcld
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR )
138 137 rexrd
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR* )
139 138 adantr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR* )
140 120 136 readdcld
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR )
141 140 rexrd
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* )
142 141 adantr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* )
143 simpr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
144 ioogtlb
 |-  ( ( ( ( Q ` i ) + ( l x. T ) ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) < t )
145 139 142 143 144 syl3anc
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) < t )
146 133 adantr
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) e. RR )
147 146 131 124 ltaddsubd
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( ( Q ` i ) + ( l x. T ) ) < t <-> ( Q ` i ) < ( t - ( l x. T ) ) ) )
148 145 147 mpbid
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) < ( t - ( l x. T ) ) )
149 iooltub
 |-  ( ( ( ( Q ` i ) + ( l x. T ) ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) )
150 139 142 143 149 syl3anc
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) )
151 124 131 121 ltsubaddd
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( t - ( l x. T ) ) < ( Q ` ( i + 1 ) ) <-> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
152 150 151 mpbird
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) < ( Q ` ( i + 1 ) ) )
153 116 122 132 148 152 eliood
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
154 100 103 153 syl2anc
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( t - ( l x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
155 98 154 sseldd
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( t - ( l x. T ) ) e. dom G )
156 elioore
 |-  ( t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -> t e. RR )
157 recn
 |-  ( t e. RR -> t e. CC )
158 157 adantl
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> t e. CC )
159 zcn
 |-  ( l e. ZZ -> l e. CC )
160 159 ad2antlr
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> l e. CC )
161 129 recnd
 |-  ( ph -> T e. CC )
162 161 ad2antrr
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> T e. CC )
163 160 162 mulcld
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( l x. T ) e. CC )
164 158 163 npcand
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) = t )
165 164 eqcomd
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> t = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
166 165 adantr
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> t = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
167 ovex
 |-  ( t - ( l x. T ) ) e. _V
168 eleq1
 |-  ( s = ( t - ( l x. T ) ) -> ( s e. dom G <-> ( t - ( l x. T ) ) e. dom G ) )
169 168 anbi2d
 |-  ( s = ( t - ( l x. T ) ) -> ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) <-> ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) ) )
170 oveq1
 |-  ( s = ( t - ( l x. T ) ) -> ( s + ( l x. T ) ) = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
171 170 eleq1d
 |-  ( s = ( t - ( l x. T ) ) -> ( ( s + ( l x. T ) ) e. dom G <-> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G ) )
172 170 fveq2d
 |-  ( s = ( t - ( l x. T ) ) -> ( G ` ( s + ( l x. T ) ) ) = ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) )
173 fveq2
 |-  ( s = ( t - ( l x. T ) ) -> ( G ` s ) = ( G ` ( t - ( l x. T ) ) ) )
174 172 173 eqeq12d
 |-  ( s = ( t - ( l x. T ) ) -> ( ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) <-> ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) )
175 171 174 anbi12d
 |-  ( s = ( t - ( l x. T ) ) -> ( ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) <-> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) ) )
176 169 175 imbi12d
 |-  ( s = ( t - ( l x. T ) ) -> ( ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) -> ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) ) <-> ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) ) ) )
177 ax-resscn
 |-  RR C_ CC
178 177 a1i
 |-  ( ph -> RR C_ CC )
179 1 178 fssd
 |-  ( ph -> F : RR --> CC )
180 179 adantr
 |-  ( ( ph /\ l e. ZZ ) -> F : RR --> CC )
181 125 adantl
 |-  ( ( ph /\ l e. ZZ ) -> l e. RR )
182 129 adantr
 |-  ( ( ph /\ l e. ZZ ) -> T e. RR )
183 181 182 remulcld
 |-  ( ( ph /\ l e. ZZ ) -> ( l x. T ) e. RR )
184 179 ad2antrr
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> F : RR --> CC )
185 129 ad2antrr
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> T e. RR )
186 simplr
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> l e. ZZ )
187 simpr
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> s e. RR )
188 9 ad4ant14
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
189 184 185 186 187 188 fperiodmul
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> ( F ` ( s + ( l x. T ) ) ) = ( F ` s ) )
190 180 183 189 2 fperdvper
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) -> ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) )
191 167 176 190 vtocl
 |-  ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) )
192 191 simpld
 |-  ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G )
193 192 adantlr
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G )
194 166 193 eqeltrd
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> t e. dom G )
195 194 ex
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
196 156 195 sylan2
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
197 196 adantlrl
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
198 197 3adantl3
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
199 155 198 mpd
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. dom G )
200 199 ralrimiva
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> A. t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) t e. dom G )
201 dfss3
 |-  ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G <-> A. t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) t e. dom G )
202 200 201 sylibr
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G )
203 202 3exp
 |-  ( ph -> ( ( i e. ( 0 ..^ M ) /\ l e. ZZ ) -> ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G ) ) )
204 203 rexlimdvv
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G ) )
205 82 204 mpd
 |-  ( ph -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G )
206 205 sselda
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> s e. dom G )
207 206 iftrued
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
208 41 207 eqtr2d
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( G ` s ) = ( H ` s ) )
209 208 mpteq2dva
 |-  ( ph -> ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( G ` s ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( H ` s ) ) )
210 28 a1i
 |-  ( ph -> dom G = dom ( RR _D F ) )
211 210 feq2d
 |-  ( ph -> ( G : dom G --> RR <-> G : dom ( RR _D F ) --> RR ) )
212 25 211 mpbird
 |-  ( ph -> G : dom G --> RR )
213 212 205 feqresmpt
 |-  ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( G ` s ) ) )
214 38 15 fmptd
 |-  ( ph -> H : RR --> RR )
215 214 17 feqresmpt
 |-  ( ph -> ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( H ` s ) ) )
216 209 213 215 3eqtr4d
 |-  ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) )
217 214 178 fssd
 |-  ( ph -> H : RR --> CC )
218 15 a1i
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) ) )
219 eleq1
 |-  ( s = ( x + T ) -> ( s e. dom G <-> ( x + T ) e. dom G ) )
220 fveq2
 |-  ( s = ( x + T ) -> ( G ` s ) = ( G ` ( x + T ) ) )
221 219 220 ifbieq1d
 |-  ( s = ( x + T ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
222 179 129 9 2 fperdvper
 |-  ( ( ph /\ x e. dom G ) -> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) )
223 222 simpld
 |-  ( ( ph /\ x e. dom G ) -> ( x + T ) e. dom G )
224 223 iftrued
 |-  ( ( ph /\ x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) = ( G ` ( x + T ) ) )
225 221 224 sylan9eqr
 |-  ( ( ( ph /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` ( x + T ) ) )
226 225 adantllr
 |-  ( ( ( ( ph /\ x e. RR ) /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` ( x + T ) ) )
227 simpr
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
228 129 adantr
 |-  ( ( ph /\ x e. RR ) -> T e. RR )
229 227 228 readdcld
 |-  ( ( ph /\ x e. RR ) -> ( x + T ) e. RR )
230 229 adantr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( x + T ) e. RR )
231 212 ad2antrr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> G : dom G --> RR )
232 223 adantlr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( x + T ) e. dom G )
233 231 232 ffvelrnd
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` ( x + T ) ) e. RR )
234 218 226 230 233 fvmptd
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` ( x + T ) ) = ( G ` ( x + T ) ) )
235 222 simprd
 |-  ( ( ph /\ x e. dom G ) -> ( G ` ( x + T ) ) = ( G ` x ) )
236 235 adantlr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` ( x + T ) ) = ( G ` x ) )
237 eleq1
 |-  ( s = x -> ( s e. dom G <-> x e. dom G ) )
238 fveq2
 |-  ( s = x -> ( G ` s ) = ( G ` x ) )
239 237 238 ifbieq1d
 |-  ( s = x -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( x e. dom G , ( G ` x ) , 0 ) )
240 239 adantl
 |-  ( ( ( ( ph /\ x e. RR ) /\ x e. dom G ) /\ s = x ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( x e. dom G , ( G ` x ) , 0 ) )
241 simplr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> x e. RR )
242 simpr
 |-  ( ( ph /\ x e. dom G ) -> x e. dom G )
243 242 iftrued
 |-  ( ( ph /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = ( G ` x ) )
244 212 ffvelrnda
 |-  ( ( ph /\ x e. dom G ) -> ( G ` x ) e. RR )
245 243 244 eqeltrd
 |-  ( ( ph /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) e. RR )
246 245 adantlr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) e. RR )
247 218 240 241 246 fvmptd
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` x ) = if ( x e. dom G , ( G ` x ) , 0 ) )
248 simpr
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> x e. dom G )
249 248 iftrued
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = ( G ` x ) )
250 247 249 eqtr2d
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` x ) = ( H ` x ) )
251 234 236 250 3eqtrd
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` ( x + T ) ) = ( H ` x ) )
252 229 recnd
 |-  ( ( ph /\ x e. RR ) -> ( x + T ) e. CC )
253 228 recnd
 |-  ( ( ph /\ x e. RR ) -> T e. CC )
254 252 253 negsubd
 |-  ( ( ph /\ x e. RR ) -> ( ( x + T ) + -u T ) = ( ( x + T ) - T ) )
255 227 recnd
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
256 255 253 pncand
 |-  ( ( ph /\ x e. RR ) -> ( ( x + T ) - T ) = x )
257 254 256 eqtr2d
 |-  ( ( ph /\ x e. RR ) -> x = ( ( x + T ) + -u T ) )
258 257 adantr
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> x = ( ( x + T ) + -u T ) )
259 simpr
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( x + T ) e. dom G )
260 simpll
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ph )
261 260 259 jca
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ph /\ ( x + T ) e. dom G ) )
262 eleq1
 |-  ( y = ( x + T ) -> ( y e. dom G <-> ( x + T ) e. dom G ) )
263 262 anbi2d
 |-  ( y = ( x + T ) -> ( ( ph /\ y e. dom G ) <-> ( ph /\ ( x + T ) e. dom G ) ) )
264 oveq1
 |-  ( y = ( x + T ) -> ( y + -u T ) = ( ( x + T ) + -u T ) )
265 264 eleq1d
 |-  ( y = ( x + T ) -> ( ( y + -u T ) e. dom G <-> ( ( x + T ) + -u T ) e. dom G ) )
266 264 fveq2d
 |-  ( y = ( x + T ) -> ( G ` ( y + -u T ) ) = ( G ` ( ( x + T ) + -u T ) ) )
267 fveq2
 |-  ( y = ( x + T ) -> ( G ` y ) = ( G ` ( x + T ) ) )
268 266 267 eqeq12d
 |-  ( y = ( x + T ) -> ( ( G ` ( y + -u T ) ) = ( G ` y ) <-> ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) )
269 265 268 anbi12d
 |-  ( y = ( x + T ) -> ( ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) <-> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) )
270 263 269 imbi12d
 |-  ( y = ( x + T ) -> ( ( ( ph /\ y e. dom G ) -> ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) ) <-> ( ( ph /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) ) )
271 129 renegcld
 |-  ( ph -> -u T e. RR )
272 161 mulm1d
 |-  ( ph -> ( -u 1 x. T ) = -u T )
273 272 eqcomd
 |-  ( ph -> -u T = ( -u 1 x. T ) )
274 273 adantr
 |-  ( ( ph /\ y e. RR ) -> -u T = ( -u 1 x. T ) )
275 274 oveq2d
 |-  ( ( ph /\ y e. RR ) -> ( y + -u T ) = ( y + ( -u 1 x. T ) ) )
276 275 fveq2d
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + -u T ) ) = ( F ` ( y + ( -u 1 x. T ) ) ) )
277 179 adantr
 |-  ( ( ph /\ y e. RR ) -> F : RR --> CC )
278 129 adantr
 |-  ( ( ph /\ y e. RR ) -> T e. RR )
279 1zzd
 |-  ( ( ph /\ y e. RR ) -> 1 e. ZZ )
280 279 znegcld
 |-  ( ( ph /\ y e. RR ) -> -u 1 e. ZZ )
281 simpr
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
282 9 adantlr
 |-  ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
283 277 278 280 281 282 fperiodmul
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + ( -u 1 x. T ) ) ) = ( F ` y ) )
284 276 283 eqtrd
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + -u T ) ) = ( F ` y ) )
285 179 271 284 2 fperdvper
 |-  ( ( ph /\ y e. dom G ) -> ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) )
286 270 285 vtoclg
 |-  ( ( x + T ) e. dom G -> ( ( ph /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) )
287 259 261 286 sylc
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) )
288 287 simpld
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ( x + T ) + -u T ) e. dom G )
289 258 288 eqeltrd
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> x e. dom G )
290 289 stoic1a
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> -. ( x + T ) e. dom G )
291 290 iffalsed
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) = 0 )
292 15 a1i
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) ) )
293 221 adantl
 |-  ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
294 229 adantr
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( x + T ) e. RR )
295 0red
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> 0 e. RR )
296 291 295 eqeltrd
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) e. RR )
297 292 293 294 296 fvmptd
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` ( x + T ) ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
298 simpr
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> -. x e. dom G )
299 298 iffalsed
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = 0 )
300 239 299 sylan9eqr
 |-  ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = x ) -> if ( s e. dom G , ( G ` s ) , 0 ) = 0 )
301 simplr
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> x e. RR )
302 292 300 301 295 fvmptd
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` x ) = 0 )
303 291 297 302 3eqtr4d
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` ( x + T ) ) = ( H ` x ) )
304 251 303 pm2.61dan
 |-  ( ( ph /\ x e. RR ) -> ( H ` ( x + T ) ) = ( H ` x ) )
305 elioore
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
306 305 adantl
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
307 305 38 sylan2
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
308 306 307 40 syl2anc
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
309 308 adantlr
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
310 94 iftrued
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
311 309 310 eqtrd
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = ( G ` s ) )
312 311 mpteq2dva
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( G ` s ) ) )
313 214 adantr
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> H : RR --> RR )
314 ioossre
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
315 314 a1i
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
316 313 315 feqresmpt
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) )
317 212 adantr
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> G : dom G --> RR )
318 317 97 feqresmpt
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( G ` s ) ) )
319 312 316 318 3eqtr4d
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
320 319 10 eqeltrd
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
321 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 ) ) ) } )
322 oveq1
 |-  ( z = y -> ( z + ( l x. T ) ) = ( y + ( l x. T ) ) )
323 322 eleq1d
 |-  ( z = y -> ( ( z + ( l x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
324 323 rexbidv
 |-  ( z = y -> ( E. l e. ZZ ( z + ( l x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) )
325 324 cbvrabv
 |-  { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q }
326 325 uneq2i
 |-  ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } )
327 326 eqcomi
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } )
328 60 fveq2i
 |-  ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) )
329 328 oveq1i
 |-  ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 )
330 isoeq5
 |-  ( ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) )
331 67 330 ax-mp
 |-  ( g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
332 331 iotabii
 |-  ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
333 isoeq1
 |-  ( f = g -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) )
334 333 cbviotavw
 |-  ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) )
335 332 334 14 3eqtr4ri
 |-  V = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) )
336 id
 |-  ( v = x -> v = x )
337 oveq2
 |-  ( v = x -> ( B - v ) = ( B - x ) )
338 337 oveq1d
 |-  ( v = x -> ( ( B - v ) / T ) = ( ( B - x ) / T ) )
339 338 fveq2d
 |-  ( v = x -> ( |_ ` ( ( B - v ) / T ) ) = ( |_ ` ( ( B - x ) / T ) ) )
340 339 oveq1d
 |-  ( v = x -> ( ( |_ ` ( ( B - v ) / T ) ) x. T ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
341 336 340 oveq12d
 |-  ( v = x -> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
342 341 cbvmptv
 |-  ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
343 eqeq1
 |-  ( u = z -> ( u = B <-> z = B ) )
344 id
 |-  ( u = z -> u = z )
345 343 344 ifbieq2d
 |-  ( u = z -> if ( u = B , A , u ) = if ( z = B , A , z ) )
346 345 cbvmptv
 |-  ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) = ( z e. ( A (,] B ) |-> if ( z = B , A , z ) )
347 eqid
 |-  ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) = ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) )
348 eqid
 |-  ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) = ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) )
349 eqid
 |-  ( z e. ( ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) (,) ( ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) |-> ( ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ` ( z - ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) ) = ( z e. ( ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) (,) ( ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) |-> ( ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ` ( z - ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) )
350 fveq2
 |-  ( i = t -> ( Q ` i ) = ( Q ` t ) )
351 350 breq1d
 |-  ( i = t -> ( ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) <-> ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) ) )
352 351 cbvrabv
 |-  { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } = { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) }
353 fveq2
 |-  ( w = x -> ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) = ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) )
354 353 fveq2d
 |-  ( w = x -> ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) = ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) )
355 354 eqcomd
 |-  ( w = x -> ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) = ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) )
356 355 breq2d
 |-  ( w = x -> ( ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) <-> ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) ) )
357 356 rabbidv
 |-  ( w = x -> { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } = { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } )
358 352 357 eqtr2id
 |-  ( w = x -> { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } )
359 358 supeq1d
 |-  ( w = x -> sup ( { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } , RR , < ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
360 359 cbvmptv
 |-  ( w e. RR |-> sup ( { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } , RR , < ) ) = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
361 3 6 7 8 217 304 320 11 12 321 327 329 335 342 346 13 347 348 349 360 fourierdlem90
 |-  ( ph -> ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )
362 216 361 eqeltrd
 |-  ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )