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 ⊢ φ → A ∈ ℝ
cncfshiftioo.b ⊢ φ → B ∈ ℝ
cncfshiftioo.c ⊢ C = A B
cncfshiftioo.t ⊢ φ → T ∈ ℝ
cncfshiftioo.d ⊢ D = A + T B + T
cncfshiftioo.f ⊢ φ → F : C ⟶cn ℂ
cncfshiftioo.g ⊢ G = x ∈ D ⟼ F ⁡ x − T
Assertion cncfshiftioo ⊢ φ → G : D ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 cncfshiftioo.a ⊢ φ → A ∈ ℝ
2 cncfshiftioo.b ⊢ φ → B ∈ ℝ
3 cncfshiftioo.c ⊢ C = A B
4 cncfshiftioo.t ⊢ φ → T ∈ ℝ
5 cncfshiftioo.d ⊢ D = A + T B + T
6 cncfshiftioo.f ⊢ φ → F : C ⟶cn ℂ
7 cncfshiftioo.g ⊢ G = x ∈ D ⟼ F ⁡ x − T
8 ioosscn ⊢ A B ⊆ ℂ
9 8 a1i ⊢ φ → A B ⊆ ℂ
10 4 recnd ⊢ φ → T ∈ ℂ
11 eqeq1 ⊢ w = x → w = z + T ↔ x = z + T
12 11 rexbidv ⊢ w = x → ∃ z ∈ A B w = z + T ↔ ∃ z ∈ 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 ⊢ ∃ z ∈ A B x = z + T ↔ ∃ y ∈ A B x = y + T
16 12 15 bitrdi ⊢ w = x → ∃ z ∈ A B w = z + T ↔ ∃ y ∈ A B x = y + T
17 16 cbvrabv ⊢ w ∈ ℂ | ∃ z ∈ A B w = z + T = x ∈ ℂ | ∃ y ∈ A B x = y + T
18 3 oveq1i ⊢ C ⟶cn ℂ = A B ⟶cn ℂ
19 6 18 eleqtrdi ⊢ φ → F : A B ⟶cn ℂ
20 eqid ⊢ x ∈ w ∈ ℂ | ∃ z ∈ A B w = z + T ⟼ F ⁡ x − T = x ∈ w ∈ ℂ | ∃ z ∈ A B w = z + T ⟼ F ⁡ x − T
21 9 10 17 19 20 cncfshift ⊢ φ → x ∈ w ∈ ℂ | ∃ z ∈ A B w = z + T ⟼ F ⁡ x − T : w ∈ ℂ | ∃ z ∈ A B w = z + T ⟶cn ℂ
22 1 2 4 iooshift ⊢ φ → A + T B + T = w ∈ ℂ | ∃ z ∈ A B w = z + T
23 5 22 syl5eq ⊢ φ → D = w ∈ ℂ | ∃ z ∈ A B w = z + T
24 23 mpteq1d ⊢ φ → x ∈ D ⟼ F ⁡ x − T = x ∈ w ∈ ℂ | ∃ z ∈ A B w = z + T ⟼ F ⁡ x − T
25 7 24 syl5eq ⊢ φ → G = x ∈ w ∈ ℂ | ∃ z ∈ A B w = z + T ⟼ F ⁡ x − T
26 23 oveq1d ⊢ φ → D ⟶cn ℂ = w ∈ ℂ | ∃ z ∈ A B w = z + T ⟶cn ℂ
27 21 25 26 3eltr4d ⊢ φ → G : D ⟶cn ℂ