Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem97 Structured version   Unicode version

Theorem fourierdlem97 32228
Description:  F is continuous on the intervals induced by the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
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
Ref Expression
fourierdlem97  |-  ( ph  ->  ( G  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  e.  ( ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) )
-cn-> CC ) )
Distinct variable groups:    A, i, x    A, m, p, i    B, i, x    B, m, p    y, C, g    C, i, x, y    C, m, p, y    y, D, g    D, i, x    D, m, p    F, s, x   
y, F    i, G, s    y, G    i, H, s, x    h, J, k, i, x    J, s   
h, M, i, x   
m, M, p    M, s    Q, h, k, g, y    Q, i, x    Q, m, p, k    Q, s    T, h, k, g, y    T, i, x    T, m, p    T, s    h, V, k, g    i, V, x    V, p    V, s    ph, h, y, g    ph, i,
s, x
Allowed substitution hints:    ph( k, m, p)    A( y, g, h, k, s)    B( y, g, h, k, s)    C( h, k, s)    D( h, k, s)    P( x, y, g, h, i, k, m, s, p)    F( g, h, i, k, m, p)    G( x, g, h, k, m, p)    H( y, g, h, k, m, p)    J( y,
g, m, p)    M( y, g, k)    V( y, m)

Proof of Theorem fourierdlem97
Dummy variables  f 
l  t  u  w  z  v  e  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ioossre 11589 . . . . . . . 8  |-  ( ( V `  J ) (,) ( V `  ( J  +  1
) ) )  C_  RR
21a1i 11 . . . . . . 7  |-  ( ph  ->  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  RR )
32sselda 3489 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  s  e.  RR )
4 iftrue 3935 . . . . . . . . . . 11  |-  ( s  e.  dom  G  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
54adantl 464 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  dom  G )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
6 fourierdlem97.f . . . . . . . . . . . . . 14  |-  ( ph  ->  F : RR --> RR )
7 ssid 3508 . . . . . . . . . . . . . 14  |-  RR  C_  RR
8 dvfre 22523 . . . . . . . . . . . . . 14  |-  ( ( F : RR --> RR  /\  RR  C_  RR )  -> 
( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
96, 7, 8sylancl 660 . . . . . . . . . . . . 13  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
10 fourierdlem97.g . . . . . . . . . . . . . 14  |-  G  =  ( RR  _D  F
)
1110feq1i 5705 . . . . . . . . . . . . 13  |-  ( G : dom  ( RR 
_D  F ) --> RR  <->  ( RR  _D  F ) : dom  ( RR 
_D  F ) --> RR )
129, 11sylibr 212 . . . . . . . . . . . 12  |-  ( ph  ->  G : dom  ( RR  _D  F ) --> RR )
1312adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  dom  G )  ->  G : dom  ( RR  _D  F ) --> RR )
14 id 22 . . . . . . . . . . . . 13  |-  ( s  e.  dom  G  -> 
s  e.  dom  G
)
1510dmeqi 5193 . . . . . . . . . . . . 13  |-  dom  G  =  dom  ( RR  _D  F )
1614, 15syl6eleq 2552 . . . . . . . . . . . 12  |-  ( s  e.  dom  G  -> 
s  e.  dom  ( RR  _D  F ) )
1716adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  dom  G )  ->  s  e.  dom  ( RR  _D  F ) )
1813, 17ffvelrnd 6008 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  dom  G )  ->  ( G `  s )  e.  RR )
195, 18eqeltrd 2542 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  dom  G )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
2019adantlr 712 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR )  /\  s  e.  dom  G )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
21 iffalse 3938 . . . . . . . . . 10  |-  ( -.  s  e.  dom  G  ->  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 )  =  0 )
22 0red 9586 . . . . . . . . . 10  |-  ( -.  s  e.  dom  G  ->  0  e.  RR )
2321, 22eqeltrd 2542 . . . . . . . . 9  |-  ( -.  s  e.  dom  G  ->  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 )  e.  RR )
2423adantl 464 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR )  /\  -.  s  e.  dom  G )  ->  if ( s  e.  dom  G , 
( G `  s
) ,  0 )  e.  RR )
2520, 24pm2.61dan 789 . . . . . . 7  |-  ( (
ph  /\  s  e.  RR )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
263, 25syldan 468 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
27 fourierdlem97.h . . . . . . 7  |-  H  =  ( s  e.  RR  |->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 ) )
2827fvmpt2 5939 . . . . . 6  |-  ( ( s  e.  RR  /\  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )  ->  ( H `  s )  =  if ( s  e.  dom  G ,  ( G `  s ) ,  0 ) )
293, 26, 28syl2anc 659 . . . . 5  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( H `  s )  =  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 ) )
30 fourierdlem97.t . . . . . . . . . 10  |-  T  =  ( B  -  A
)
31 fourierdlem97.p . . . . . . . . . 10  |-  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 ) ) ) } )
32 fourierdlem97.m . . . . . . . . . 10  |-  ( ph  ->  M  e.  NN )
33 fourierdlem97.q . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ( P `
 M ) )
34 fourierdlem97.c . . . . . . . . . 10  |-  ( ph  ->  C  e.  RR )
35 fourierdlem97.d . . . . . . . . . . 11  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
36 elioore 11562 . . . . . . . . . . 11  |-  ( D  e.  ( C (,) +oo )  ->  D  e.  RR )
3735, 36syl 16 . . . . . . . . . 10  |-  ( ph  ->  D  e.  RR )
3834rexrd 9632 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  RR* )
39 pnfxr 11324 . . . . . . . . . . . 12  |- +oo  e.  RR*
4039a1i 11 . . . . . . . . . . 11  |-  ( ph  -> +oo  e.  RR* )
41 ioogtlb 31770 . . . . . . . . . . 11  |-  ( ( C  e.  RR*  /\ +oo  e.  RR*  /\  D  e.  ( C (,) +oo ) )  ->  C  <  D )
4238, 40, 35, 41syl3anc 1226 . . . . . . . . . 10  |-  ( ph  ->  C  <  D )
43 oveq1 6277 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
y  +  ( h  x.  T ) )  =  ( x  +  ( h  x.  T
) ) )
4443eleq1d 2523 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
( y  +  ( h  x.  T ) )  e.  ran  Q  <->  ( x  +  ( h  x.  T ) )  e.  ran  Q ) )
4544rexbidv 2965 . . . . . . . . . . . 12  |-  ( y  =  x  ->  ( E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q  <->  E. h  e.  ZZ  (
x  +  ( h  x.  T ) )  e.  ran  Q ) )
4645cbvrabv 3105 . . . . . . . . . . 11  |-  { 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 }
4746uneq2i 3641 . . . . . . . . . 10  |-  ( { 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 } )
48 oveq1 6277 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  l  ->  (
k  x.  T )  =  ( l  x.  T ) )
4948oveq2d 6286 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  l  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( l  x.  T
) ) )
5049eleq1d 2523 . . . . . . . . . . . . . . . . 17  |-  ( k  =  l  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( l  x.  T ) )  e.  ran  Q ) )
5150cbvrexv 3082 . . . . . . . . . . . . . . . 16  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. l  e.  ZZ  ( y  +  ( l  x.  T
) )  e.  ran  Q )
5251a1i 11 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
5352rabbiia 3095 . . . . . . . . . . . . . 14  |-  { 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 }
5453uneq2i 3641 . . . . . . . . . . . . 13  |-  ( { 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 } )
55 oveq1 6277 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  h  ->  (
l  x.  T )  =  ( h  x.  T ) )
5655oveq2d 6286 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  h  ->  (
y  +  ( l  x.  T ) )  =  ( y  +  ( h  x.  T
) ) )
5756eleq1d 2523 . . . . . . . . . . . . . . . . 17  |-  ( l  =  h  ->  (
( y  +  ( l  x.  T ) )  e.  ran  Q  <->  ( y  +  ( h  x.  T ) )  e.  ran  Q ) )
5857cbvrexv 3082 . . . . . . . . . . . . . . . 16  |-  ( E. l  e.  ZZ  (
y  +  ( l  x.  T ) )  e.  ran  Q  <->  E. h  e.  ZZ  ( y  +  ( h  x.  T
) )  e.  ran  Q )
5958a1i 11 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
6059rabbiia 3095 . . . . . . . . . . . . . 14  |-  { 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 }
6160uneq2i 3641 . . . . . . . . . . . . 13  |-  ( { 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 } )
6254, 61eqtri 2483 . . . . . . . . . . . 12  |-  ( { 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 } )
6362fveq2i 5851 . . . . . . . . . . 11  |-  ( # `  ( { 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 } ) )
6463oveq1i 6280 . . . . . . . . . 10  |-  ( (
# `  ( { 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 )
65 fourierdlem97.v . . . . . . . . . 10  |-  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 }
) ) )
66 fourierdlem97.j . . . . . . . . . 10  |-  ( ph  ->  J  e.  ( 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) )
67 oveq1 6277 . . . . . . . . . . . . . 14  |-  ( k  =  h  ->  (
k  x.  T )  =  ( h  x.  T ) )
6867oveq2d 6286 . . . . . . . . . . . . 13  |-  ( k  =  h  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( h  x.  T
) ) )
6968breq1d 4449 . . . . . . . . . . . 12  |-  ( k  =  h  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( h  x.  T ) )  <_ 
( V `  J
) ) )
7069cbvrabv 3105 . . . . . . . . . . 11  |-  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) }  =  { h  e.  ZZ  |  ( ( Q `
 0 )  +  ( h  x.  T
) )  <_  ( V `  J ) }
7170supeq1i 7898 . . . . . . . . . 10  |-  sup ( { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  )  =  sup ( { h  e.  ZZ  |  ( ( Q `
 0 )  +  ( h  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  )
72 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( j  =  e  ->  ( Q `  j )  =  ( Q `  e ) )
7372oveq1d 6285 . . . . . . . . . . . . 13  |-  ( 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
) ) )
7473breq1d 4449 . . . . . . . . . . . 12  |-  ( 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
) ) )
7574cbvrabv 3105 . . . . . . . . . . 11  |-  { 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
) }
7675supeq1i 7898 . . . . . . . . . 10  |-  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 ,  <  )
7730, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76fourierdlem64 32195 . . . . . . . . 9  |-  ( 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
) ) ) ) )
7877simprd 461 . . . . . . . 8  |-  ( 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 ) ) ) )
79 simpl1 997 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
80 simpl2l 1047 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
81 fourierdlem97.qcn . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
82 cncff 21566 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 )
8381, 82syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
84 ffun 5715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G : dom  ( RR 
_D  F ) --> RR 
->  Fun  G )
8512, 84syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Fun  G )
8685adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Fun  G )
87 ffvresb 6038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
8886, 87syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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 ) ) )
8983, 88mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( s  e.  dom  G  /\  ( G `  s )  e.  CC ) )
9089r19.21bi 2823 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
s  e.  dom  G  /\  ( G `  s
)  e.  CC ) )
9190simpld 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  dom  G )
9291ralrimiva 2868 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) s  e.  dom  G
)
93 dfss3 3479 . . . . . . . . . . . . . . . 16  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  G  <->  A. s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) s  e.  dom  G )
9492, 93sylibr 212 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  G )
9579, 80, 94syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
96 simpl2 998 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
)
9779, 96jca 530 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
98 simpl3 999 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) ) )
99 simpr 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) ) )
10098, 99sseldd 3490 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) ) )
10131fourierdlem2 32133 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) ) ) ) )
10232, 101syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) ) ) )
10333, 102mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
104103simpld 457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
105 elmapi 7433 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
106104, 105syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
107106adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
108 elfzofz 11819 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
109108adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
110107, 109ffvelrnd 6008 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
111110rexrd 9632 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
112111adantrr 714 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  ( Q `  i )  e.  RR* )
113112adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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* )
114 fzofzp1 11890 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
115114adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
116107, 115ffvelrnd 6008 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
117116adantrr 714 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
118117adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
119118rexrd 9632 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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* )
120 elioore 11562 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ( ( ( Q `  i )  +  ( l  x.  T ) ) (,) ( ( Q `  ( i  +  1 ) )  +  ( l  x.  T ) ) )  ->  t  e.  RR )
121120adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  /\  t  e.  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  t  e.  RR )
122 zre 10864 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  e.  ZZ  ->  l  e.  RR )
123122adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ M )  /\  l  e.  ZZ )  ->  l  e.  RR )
124123ad2antlr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  /\  t  e.  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  l  e.  RR )
125 fourierdlem97.a . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR )
126 fourierdlem97.b . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  RR )
127125, 126resubcld 9983 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( B  -  A
)  e.  RR )
12830, 127syl5eqel 2546 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  T  e.  RR )
129128ad2antrr 723 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  /\  t  e.  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  T  e.  RR )
130124, 129remulcld 9613 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
131121, 130resubcld 9983 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
132110adantrr 714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  ( Q `  i )  e.  RR )
133122ad2antll 726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  l  e.  RR )
134128adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  T  e.  RR )
135133, 134remulcld 9613 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
l  x.  T )  e.  RR )
136132, 135readdcld 9612 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  i
)  +  ( l  x.  T ) )  e.  RR )
137136rexrd 9632 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  i
)  +  ( l  x.  T ) )  e.  RR* )
138137adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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* )
139117, 135readdcld 9612 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  (
i  +  1 ) )  +  ( l  x.  T ) )  e.  RR )
140139rexrd 9632 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  (
i  +  1 ) )  +  ( l  x.  T ) )  e.  RR* )
141140adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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* )
142 simpr 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) ) )
143 ioogtlb 31770 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
144138, 141, 142, 143syl3anc 1226 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
)
145132adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
146145, 130, 121ltaddsubd 10148 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) )
147144, 146mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
148 iooltub 31790 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) ) )
149138, 141, 142, 148syl3anc 1226 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
150121, 130, 118ltsubaddd 10144 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) )
151149, 150mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
152113, 119, 131, 147, 151eliood 31773 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
15397, 100, 152syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
15495, 153sseldd 3490 . . . . . . . . . . . . 13  |-  ( ( ( 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
)
155 elioore 11562 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  ->  t  e.  RR )
156 recn 9571 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  RR  ->  t  e.  CC )
157156adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  t  e.  CC )
158 zcn 10865 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  e.  ZZ  ->  l  e.  CC )
159158ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  l  e.  CC )
160128recnd 9611 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  T  e.  CC )
161160ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  T  e.  CC )
162159, 161mulcld 9605 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  (
l  x.  T )  e.  CC )
163157, 162npcand 9926 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  (
( t  -  (
l  x.  T ) )  +  ( l  x.  T ) )  =  t )
164163eqcomd 2462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  t  =  ( ( t  -  ( l  x.  T ) )  +  ( l  x.  T
) ) )
165164adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G )  ->  t  =  ( ( t  -  ( l  x.  T
) )  +  ( l  x.  T ) ) )
166 ovex 6298 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  -  ( l  x.  T ) )  e. 
_V
167 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
s  e.  dom  G  <->  ( t  -  ( l  x.  T ) )  e.  dom  G ) )
168167anbi2d 701 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
( ( ph  /\  l  e.  ZZ )  /\  s  e.  dom  G )  <->  ( ( ph  /\  l  e.  ZZ )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G ) ) )
169 oveq1 6277 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
s  +  ( l  x.  T ) )  =  ( ( t  -  ( l  x.  T ) )  +  ( l  x.  T
) ) )
170169eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
( s  +  ( l  x.  T ) )  e.  dom  G  <->  ( ( t  -  (
l  x.  T ) )  +  ( l  x.  T ) )  e.  dom  G ) )
171169fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  ( G `  ( s  +  ( l  x.  T ) ) )  =  ( G `  ( ( t  -  ( l  x.  T
) )  +  ( l  x.  T ) ) ) )
172 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  ( G `  s )  =  ( G `  ( t  -  (
l  x.  T ) ) ) )
173171, 172eqeq12d 2476 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) ) ) )
174170, 173anbi12d 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) ) ) )
175168, 174imbi12d 318 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) ) ) ) )
176 ax-resscn 9538 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  RR  C_  CC
177176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  RR  C_  CC )
1786, 177fssd 5722 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F : RR --> CC )
179178adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  l  e.  ZZ )  ->  F : RR
--> CC )
180122adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  l  e.  ZZ )  ->  l  e.  RR )
181128adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  l  e.  ZZ )  ->  T  e.  RR )
182180, 181remulcld 9613 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  l  e.  ZZ )  ->  ( l  x.  T )  e.  RR )
183178ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  F : RR --> CC )
184128ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  T  e.  RR )
185 simplr 753 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  l  e.  ZZ )
186 simpr 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  s  e.  RR )
187 fourierdlem97.fper . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
188187adant423 31668 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
189183, 184, 185, 186, 188fperiodmul 31746 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  ( F `  ( s  +  ( l  x.  T ) ) )  =  ( F `  s ) )
190179, 182, 189, 10fperdvper 31957 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  dom  G )  -> 
( ( s  +  ( l  x.  T
) )  e.  dom  G  /\  ( G `  ( s  +  ( l  x.  T ) ) )  =  ( G `  s ) ) )
191166, 175, 190vtocl 3158 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) ) ) )
192191simpld 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  (
t  -  ( l  x.  T ) )  e.  dom  G )  ->  ( ( t  -  ( l  x.  T ) )  +  ( l  x.  T
) )  e.  dom  G )
193192adantlr 712 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G )  ->  ( (
t  -  ( l  x.  T ) )  +  ( l  x.  T ) )  e. 
dom  G )
194165, 193eqeltrd 2542 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G )  ->  t  e.  dom  G )
195194ex 432 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  (
( t  -  (
l  x.  T ) )  e.  dom  G  ->  t  e.  dom  G
) )
196155, 195sylan2 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( t  -  (
l  x.  T ) )  e.  dom  G  ->  t  e.  dom  G
) )
197196adantlrl 717 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
1981973adantl3 1152 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
199154, 198mpd 15 . . . . . . . . . . . 12  |-  ( ( ( 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
)
200199ralrimiva 2868 . . . . . . . . . . 11  |-  ( (
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 3479 . . . . . . . . . . 11  |-  ( ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) 
C_  dom  G  <->  A. t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) t  e.  dom  G )
202200, 201sylibr 212 . . . . . . . . . 10  |-  ( (
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 )
2032023exp 1193 . . . . . . . . 9  |-  ( 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 ) ) )
204203rexlimdvv 2952 . . . . . . . 8  |-  ( 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 ) )
20578, 204mpd 15 . . . . . . 7  |-  ( ph  ->  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  dom  G )
206205sselda 3489 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  s  e.  dom  G )
207206iftrued 3937 . . . . 5  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
20829, 207eqtr2d 2496 . . . 4  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( G `  s )  =  ( H `  s ) )
209208mpteq2dva 4525 . . 3  |-  ( ph  ->  ( s  e.  ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) 
|->  ( G `  s
) )  =  ( s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1
) ) )  |->  ( H `  s ) ) )
21015a1i 11 . . . . . 6  |-  ( ph  ->  dom  G  =  dom  ( RR  _D  F
) )
211210feq2d 5700 . . . . 5  |-  ( ph  ->  ( G : dom  G --> RR  <->  G : dom  ( RR  _D  F ) --> RR ) )
21212, 211mpbird 232 . . . 4  |-  ( ph  ->  G : dom  G --> RR )
213212, 205feqresmpt 5902 . . 3  |-  ( ph  ->  ( G  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  =  ( s  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  |->  ( G `
 s ) ) )
21425, 27fmptd 6031 . . . 4  |-  ( ph  ->  H : RR --> RR )
215214, 2feqresmpt 5902 . . 3  |-  ( ph  ->  ( H  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  =  ( s  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  |->  ( H `
 s ) ) )
216209, 213, 2153eqtr4d 2505 . 2  |-  ( ph  ->  ( G  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  =  ( H  |`  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) ) )
217214, 177fssd 5722 . . 3  |-  ( ph  ->  H : RR --> CC )
21827a1i 11 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  H  =  ( s  e.  RR  |->  if ( s  e.  dom  G , 
( G `  s
) ,  0 ) ) )
219 eleq1 2526 . . . . . . . . 9  |-  ( s  =  ( x  +  T )  ->  (
s  e.  dom  G  <->  ( x  +  T )  e.  dom  G ) )
220 fveq2 5848 . . . . . . . . 9  |-  ( s  =  ( x  +  T )  ->  ( G `  s )  =  ( G `  ( x  +  T
) ) )
221219, 220ifbieq1d 3952 . . . . . . . 8  |-  ( s  =  ( x  +  T )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  if ( ( x  +  T
)  e.  dom  G ,  ( G `  ( x  +  T
) ) ,  0 ) )
222178, 128, 187, 10fperdvper 31957 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
( x  +  T
)  e.  dom  G  /\  ( G `  (
x  +  T ) )  =  ( G `
 x ) ) )
223222simpld 457 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  +  T )  e.  dom  G )
224223iftrued 3937 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  if ( ( x  +  T )  e.  dom  G ,  ( G `  ( x  +  T
) ) ,  0 )  =  ( G `
 ( x  +  T ) ) )
225221, 224sylan9eqr 2517 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  s  =  ( x  +  T ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 ( x  +  T ) ) )
226225adantllr 716 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  /\  s  =  ( x  +  T
) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 ( x  +  T ) ) )
227 simpr 459 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
228128adantr 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
229227, 228readdcld 9612 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  T )  e.  RR )
230229adantr 463 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( x  +  T
)  e.  RR )
231212ad2antrr 723 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  G : dom  G --> RR )
232223adantlr 712 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( x  +  T
)  e.  dom  G
)
233231, 232ffvelrnd 6008 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( G `  (
x  +  T ) )  e.  RR )
234218, 226, 230, 233fvmptd 5936 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( H `  (
x  +  T ) )  =  ( G `
 ( x  +  T ) ) )
235222simprd 461 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( G `  ( x  +  T ) )  =  ( G `  x
) )
236235adantlr 712 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( G `  (
x  +  T ) )  =  ( G `
 x ) )
237 eleq1 2526 . . . . . . . . 9  |-  ( s  =  x  ->  (
s  e.  dom  G  <->  x  e.  dom  G ) )
238 fveq2 5848 . . . . . . . . 9  |-  ( s  =  x  ->  ( G `  s )  =  ( G `  x ) )
239237, 238ifbieq1d 3952 . . . . . . . 8  |-  ( s  =  x  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  if ( x  e.  dom  G ,  ( G `  x ) ,  0 ) )
240239adantl 464 . . . . . . 7  |-  ( ( ( ( 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 753 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  x  e.  RR )
242 simpr 459 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  dom  G )
243242iftrued 3937 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  =  ( G `
 x ) )
244212ffvelrnda 6007 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( G `  x )  e.  RR )
245243, 244eqeltrd 2542 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  e.  RR )
246245adantlr 712 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  e.  RR )
247218, 240, 241, 246fvmptd 5936 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( H `  x
)  =  if ( x  e.  dom  G ,  ( G `  x ) ,  0 ) )
248 simpr 459 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  x  e.  dom  G )
249248iftrued 3937 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  =  ( G `
 x ) )
250247, 249eqtr2d 2496 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( G `  x
)  =  ( H `
 x ) )
251234, 236, 2503eqtrd 2499 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( H `  (
x  +  T ) )  =  ( H `
 x ) )
252229recnd 9611 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  T )  e.  CC )
253228recnd 9611 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
254252, 253negsubd 9928 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  +  T )  +  -u T )  =  ( ( x  +  T )  -  T
) )
255227recnd 9611 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
256255, 253pncand 9923 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  +  T )  -  T )  =  x )
257254, 256eqtr2d 2496 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  x  =  ( ( x  +  T )  +  -u T ) )
258257adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  x  =  ( ( x  +  T
)  +  -u T
) )
259 simpr 459 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( x  +  T )  e.  dom  G )
260 simpll 751 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ph )
261260, 259jca 530 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( ph  /\  ( x  +  T
)  e.  dom  G
) )
262 eleq1 2526 . . . . . . . . . . . . 13  |-  ( y  =  ( x  +  T )  ->  (
y  e.  dom  G  <->  ( x  +  T )  e.  dom  G ) )
263262anbi2d 701 . . . . . . . . . . . 12  |-  ( y  =  ( x  +  T )  ->  (
( ph  /\  y  e.  dom  G )  <->  ( ph  /\  ( x  +  T
)  e.  dom  G
) ) )
264 oveq1 6277 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  +  T )  ->  (
y  +  -u T
)  =  ( ( x  +  T )  +  -u T ) )
265264eleq1d 2523 . . . . . . . . . . . . 13  |-  ( y  =  ( x  +  T )  ->  (
( y  +  -u T )  e.  dom  G  <-> 
( ( x  +  T )  +  -u T )  e.  dom  G ) )
266264fveq2d 5852 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  +  T )  ->  ( G `  ( y  +  -u T ) )  =  ( G `  ( ( x  +  T )  +  -u T ) ) )
267 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  +  T )  ->  ( G `  y )  =  ( G `  ( x  +  T
) ) )
268266, 267eqeq12d 2476 . . . . . . . . . . . . 13  |-  ( y  =  ( x  +  T )  ->  (
( G `  (
y  +  -u T
) )  =  ( G `  y )  <-> 
( G `  (
( x  +  T
)  +  -u T
) )  =  ( G `  ( x  +  T ) ) ) )
269265, 268anbi12d 708 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) )
270263, 269imbi12d 318 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) )
271128renegcld 9982 . . . . . . . . . . . 12  |-  ( ph  -> 
-u T  e.  RR )
272160mulm1d 10004 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -u 1  x.  T )  =  -u T )
273272eqcomd 2462 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u T  =  (
-u 1  x.  T
) )
274273adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  -u T  =  ( -u 1  x.  T ) )
275274oveq2d 6286 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  -u T )  =  ( y  +  (
-u 1  x.  T
) ) )
276275fveq2d 5852 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  + 
-u T ) )  =  ( F `  ( y  +  (
-u 1  x.  T
) ) ) )
277178adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  F : RR
--> CC )
278128adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  T  e.  RR )
279 1zzd 10891 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  1  e.  ZZ )
280279znegcld 10967 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  -u 1  e.  ZZ )
281 simpr 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
282187adantlr 712 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
283277, 278, 280, 281, 282fperiodmul 31746 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  ( -u 1  x.  T ) ) )  =  ( F `  y ) )
284276, 283eqtrd 2495 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  + 
-u T ) )  =  ( F `  y ) )
285178, 271, 284, 10fperdvper 31957 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  dom  G )  ->  (
( y  +  -u T )  e.  dom  G  /\  ( G `  ( y  +  -u T ) )  =  ( G `  y
) ) )
286270, 285vtoclg 3164 . . . . . . . . . 10  |-  ( ( 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 ) ) ) ) )
287259, 261, 286sylc 60 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( ( ( x  +  T )  +  -u T )  e. 
dom  G  /\  ( G `  ( (
x  +  T )  +  -u T ) )  =  ( G `  ( x  +  T
) ) ) )
288287simpld 457 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( ( x  +  T )  + 
-u T )  e. 
dom  G )
289258, 288eqeltrd 2542 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  x  e.  dom  G )
290289stoic1a 1609 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  -.  ( x  +  T )  e.  dom  G )
291290iffalsed 3940 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  if ( ( x  +  T )  e.  dom  G , 
( G `  (
x  +  T ) ) ,  0 )  =  0 )
29227a1i 11 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  H  =  ( s  e.  RR  |->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 ) ) )
293221adantl 464 . . . . . 6  |-  ( ( ( ( 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 ) )
294229adantr 463 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( x  +  T )  e.  RR )
295 0red 9586 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  0  e.  RR )
296291, 295eqeltrd 2542 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  if ( ( x  +  T )  e.  dom  G , 
( G `  (
x  +  T ) ) ,  0 )  e.  RR )
297292, 293, 294, 296fvmptd 5936 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( H `  ( x  +  T
) )  =  if ( ( x  +  T )  e.  dom  G ,  ( G `  ( x  +  T
) ) ,  0 ) )
298 simpr 459 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  -.  x  e.  dom  G )
299298iffalsed 3940 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  if ( x  e.  dom  G , 
( G `  x
) ,  0 )  =  0 )
300239, 299sylan9eqr 2517 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  /\  s  =  x )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  0 )
301 simplr 753 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  x  e.  RR )
302292, 300, 301, 295fvmptd 5936 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( H `  x )  =  0 )
303291, 297, 3023eqtr4d 2505 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( H `  ( x  +  T
) )  =  ( H `  x ) )
304251, 303pm2.61dan 789 . . 3  |-  ( (
ph  /\  x  e.  RR )  ->  ( H `
 ( x  +  T ) )  =  ( H `  x
) )
305 elioore 11562 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
306305adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
307305, 25sylan2 472 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
308306, 307, 28syl2anc 659 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( H `  s )  =  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 ) )
309308adantlr 712 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( H `  s )  =  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 ) )
31091iftrued 3937 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
311309, 310eqtrd 2495 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( H `  s )  =  ( G `  s ) )
312311mpteq2dva 4525 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( H `  s ) )  =  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( G `  s
) ) )
313214adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  H : RR --> RR )
314 ioossre 11589 . . . . . . 7  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
315314a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
316313, 315feqresmpt 5902 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( H `  s ) ) )
317212adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  G : dom  G --> RR )
318317, 94feqresmpt 5902 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( G `  s ) ) )
319312, 316, 3183eqtr4d 2505 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
320319, 81eqeltrd 2542 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
321 eqid 2454 . . 3  |-  ( 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 6277 . . . . . . . 8  |-  ( z  =  y  ->  (
z  +  ( l  x.  T ) )  =  ( y  +  ( l  x.  T
) ) )
323322eleq1d 2523 . . . . . . 7  |-  ( z  =  y  ->  (
( z  +  ( l  x.  T ) )  e.  ran  Q  <->  ( y  +  ( l  x.  T ) )  e.  ran  Q ) )
324323rexbidv 2965 . . . . . 6  |-  ( z  =  y  ->  ( E. l  e.  ZZ  ( z  +  ( l  x.  T ) )  e.  ran  Q  <->  E. l  e.  ZZ  (
y  +  ( l  x.  T ) )  e.  ran  Q ) )
325324cbvrabv 3105 . . . . 5  |-  { 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 }
326325uneq2i 3641 . . . 4  |-  ( { 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 } )
327326eqcomi 2467 . . 3  |-  ( { 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 } )
32854fveq2i 5851 . . . 4  |-  ( # `  ( { 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 } ) )
329328oveq1i 6280 . . 3  |-  ( (
# `  ( { 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 6194 . . . . . 6  |-  ( ( { 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 } ) ) ) )
33161, 330ax-mp 5 . . . . 5  |-  ( 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 } ) ) )
332331iotabii 5556 . . . 4  |-  ( 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 6190 . . . . 5  |-  ( 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 } ) ) ) )
334333cbviotav 5540 . . . 4  |-  ( 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 }
) ) )
335332, 334, 653eqtr4ri 2494 . . 3  |-  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 22 . . . . 5  |-  ( v  =  x  ->  v  =  x )
337 oveq2 6278 . . . . . . . 8  |-  ( v  =  x  ->  ( B  -  v )  =  ( B  -  x ) )
338337oveq1d 6285 . . . . . . 7  |-  ( v  =  x  ->  (
( B  -  v
)  /  T )  =  ( ( B  -  x )  /  T ) )
339338fveq2d 5852 . . . . . 6  |-  ( v  =  x  ->  ( |_ `  ( ( B  -  v )  /  T ) )  =  ( |_ `  (
( B  -  x
)  /  T ) ) )
340339oveq1d 6285 . . . . 5  |-  ( v  =  x  ->  (
( |_ `  (
( B  -  v
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )
341336, 340oveq12d 6288 . . . 4  |-  ( v  =  x  ->  (
v  +  ( ( |_ `  ( ( B  -  v )  /  T ) )  x.  T ) )  =  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
342341cbvmptv 4530 . . 3  |-  ( v  e.  RR  |->  ( v  +  ( ( |_
`  ( ( B  -  v )  /  T ) )  x.  T ) ) )  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T
) )  x.  T
) ) )
343 eqeq1 2458 . . . . 5  |-  ( u  =  z  ->  (
u  =  B  <->  z  =  B ) )
344 id 22 . . . . 5  |-  ( u  =  z  ->  u  =  z )
345343, 344ifbieq2d 3954 . . . 4  |-  ( u  =  z  ->  if ( u  =  B ,  A ,  u )  =  if ( z  =  B ,  A ,  z ) )
346345cbvmptv 4530 . . 3  |-  ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u )
)  =  ( z  e.  ( A (,] B )  |->  if ( z  =  B ,  A ,  z )
)
347 eqid 2454 . . 3  |-  ( ( 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 2454 . . 3  |-  ( H  |`  ( ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u )
) `