This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem23

Description: If F is continuous and X is constant, then ( F( X + s ) ) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem23.a ⊢ φ → A ⊆ ℂ
fourierdlem23.f ⊢ φ → F : A ⟶cn ℂ
fourierdlem23.b ⊢ φ → B ⊆ ℂ
fourierdlem23.x ⊢ φ → X ∈ ℂ
fourierdlem23.xps ⊢ φ ∧ s ∈ B → X + s ∈ A
Assertion fourierdlem23 ⊢ φ → s ∈ B ⟼ F ⁡ X + s : B ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 fourierdlem23.a ⊢ φ → A ⊆ ℂ
2 fourierdlem23.f ⊢ φ → F : A ⟶cn ℂ
3 fourierdlem23.b ⊢ φ → B ⊆ ℂ
4 fourierdlem23.x ⊢ φ → X ∈ ℂ
5 fourierdlem23.xps ⊢ φ ∧ s ∈ B → X + s ∈ A
6 eqid ⊢ s ∈ B ⟼ X + s = s ∈ B ⟼ X + s
7 6 addccncf2 ⊢ B ⊆ ℂ ∧ X ∈ ℂ → s ∈ B ⟼ X + s : B ⟶cn ℂ
8 3 4 7 syl2anc ⊢ φ → s ∈ B ⟼ X + s : B ⟶cn ℂ
9 ssid ⊢ B ⊆ B
10 9 a1i ⊢ φ → B ⊆ B
11 6 8 10 1 5 cncfmptssg ⊢ φ → s ∈ B ⟼ X + s : B ⟶cn A
12 11 2 cncfcompt ⊢ φ → s ∈ B ⟼ F ⁡ X + s : B ⟶cn ℂ