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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	cncfshiftioo.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	cncfshiftioo.c	⊢ 𝐶 = ( 𝐴 (,) 𝐵 )
	cncfshiftioo.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
	cncfshiftioo.d	⊢ 𝐷 = ( ( 𝐴 + 𝑇 ) (,) ( 𝐵 + 𝑇 ) )
	cncfshiftioo.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ ℂ ) )
	cncfshiftioo.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
Assertion	cncfshiftioo	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		cncfshiftioo.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		cncfshiftioo.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		cncfshiftioo.c	⊢ 𝐶 = ( 𝐴 (,) 𝐵 )
4		cncfshiftioo.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
5		cncfshiftioo.d	⊢ 𝐷 = ( ( 𝐴 + 𝑇 ) (,) ( 𝐵 + 𝑇 ) )
6		cncfshiftioo.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ ℂ ) )
7		cncfshiftioo.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
8		ioosscn	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
9	8	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
10	4	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
11		eqeq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑧 + 𝑇 ) ) )
12	11	rexbidv	⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) )
13		oveq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 𝑇 ) = ( 𝑦 + 𝑇 ) )
14	13	eqeq2d	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑦 + 𝑇 ) ) )
15	14	cbvrexvw	⊢ ( ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑥 = ( 𝑦 + 𝑇 ) )
16	12 15	bitrdi	⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑥 = ( 𝑦 + 𝑇 ) ) )
17	16	cbvrabv	⊢ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) 𝑥 = ( 𝑦 + 𝑇 ) }
18	3	oveq1i	⊢ ( 𝐶 –cn→ ℂ ) = ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ )
19	6 18	eleqtrdi	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
20		eqid	⊢ ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) = ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
21	9 10 17 19 20	cncfshift	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) ∈ ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) )
22	1 2 4	iooshift	⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) (,) ( 𝐵 + 𝑇 ) ) = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } )
23	5 22	syl5eq	⊢ ( 𝜑 → 𝐷 = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } )
24	23	mpteq1d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) = ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) )
25	7 24	syl5eq	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) ) )
26	23	oveq1d	⊢ ( 𝜑 → ( 𝐷 –cn→ ℂ ) = ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) )
27	21 25 26	3eltr4d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 –cn→ ℂ ) )

Metamath Proof Explorer

Theorem cncfshiftioo

Proof