Metamath Proof Explorer

Theorem cncfshiftioo

Description: A periodic continuous function stays continuous if the domain is an open interval that is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfshiftioo.a 
|- ( ph -> A e. RR )
cncfshiftioo.b 
|- ( ph -> B e. RR )
cncfshiftioo.c 
|- C = ( A (,) B )
cncfshiftioo.t 
|- ( ph -> T e. RR )
cncfshiftioo.d 
|- D = ( ( A + T ) (,) ( B + T ) )
cncfshiftioo.f 
|- ( ph -> F e. ( C -cn-> CC ) )
cncfshiftioo.g 
|- G = ( x e. D |-> ( F ` ( x - T ) ) )
Assertion cncfshiftioo 
|- ( ph -> G e. ( D -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 cncfshiftioo.a 
 |-  ( ph -> A e. RR )
2 cncfshiftioo.b 
 |-  ( ph -> B e. RR )
3 cncfshiftioo.c 
 |-  C = ( A (,) B )
4 cncfshiftioo.t 
 |-  ( ph -> T e. RR )
5 cncfshiftioo.d 
 |-  D = ( ( A + T ) (,) ( B + T ) )
6 cncfshiftioo.f 
 |-  ( ph -> F e. ( C -cn-> CC ) )
7 cncfshiftioo.g 
 |-  G = ( x e. D |-> ( F ` ( x - T ) ) )
8 ioosscn 
 |-  ( A (,) B ) C_ CC
9 8 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
10 4 recnd 
 |-  ( ph -> T e. CC )
11 eqeq1 
 |-  ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
12 11 rexbidv 
 |-  ( w = x -> ( E. z e. ( A (,) B ) w = ( z + T ) <-> E. z e. ( A (,) B ) x = ( z + T ) ) )
13 oveq1 
 |-  ( z = y -> ( z + T ) = ( y + T ) )
14 13 eqeq2d 
 |-  ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
15 14 cbvrexvw 
 |-  ( E. z e. ( A (,) B ) x = ( z + T ) <-> E. y e. ( A (,) B ) x = ( y + T ) )
16 12 15 bitrdi 
 |-  ( w = x -> ( E. z e. ( A (,) B ) w = ( z + T ) <-> E. y e. ( A (,) B ) x = ( y + T ) ) )
17 16 cbvrabv 
 |-  { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } = { x e. CC | E. y e. ( A (,) B ) x = ( y + T ) }
18 3 oveq1i 
 |-  ( C -cn-> CC ) = ( ( A (,) B ) -cn-> CC )
19 6 18 eleqtrdi 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
20 eqid 
 |-  ( x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } |-> ( F ` ( x - T ) ) ) = ( x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } |-> ( F ` ( x - T ) ) )
21 9 10 17 19 20 cncfshift 
 |-  ( ph -> ( x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } |-> ( F ` ( x - T ) ) ) e. ( { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } -cn-> CC ) )
22 1 2 4 iooshift 
 |-  ( ph -> ( ( A + T ) (,) ( B + T ) ) = { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } )
23 5 22 syl5eq 
 |-  ( ph -> D = { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } )
24 23 mpteq1d 
 |-  ( ph -> ( x e. D |-> ( F ` ( x - T ) ) ) = ( x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } |-> ( F ` ( x - T ) ) ) )
25 7 24 syl5eq 
 |-  ( ph -> G = ( x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } |-> ( F ` ( x - T ) ) ) )
26 23 oveq1d 
 |-  ( ph -> ( D -cn-> CC ) = ( { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } -cn-> CC ) )
27 21 25 26 3eltr4d 
 |-  ( ph -> G e. ( D -cn-> CC ) )