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 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
fourierdlem23.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
fourierdlem23.b ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
fourierdlem23.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
fourierdlem23.xps ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑋 + 𝑠 ) ∈ 𝐴 )
Assertion fourierdlem23 ( 𝜑 → ( 𝑠 ∈ 𝐵 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( 𝐵 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem23.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2 fourierdlem23.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
3 fourierdlem23.b ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
4 fourierdlem23.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5 fourierdlem23.xps ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑋 + 𝑠 ) ∈ 𝐴 )
6 eqid ⊢ ( 𝑠 ∈ 𝐵 ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ 𝐵 ↦ ( 𝑋 + 𝑠 ) )
7 6 addccncf2 ⊢ ( ( 𝐵 ⊆ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑠 ∈ 𝐵 ↦ ( 𝑋 + 𝑠 ) ) ∈ ( 𝐵 –cn→ ℂ ) )
8 3 4 7 syl2anc ⊢ ( 𝜑 → ( 𝑠 ∈ 𝐵 ↦ ( 𝑋 + 𝑠 ) ) ∈ ( 𝐵 –cn→ ℂ ) )
9 ssid ⊢ 𝐵 ⊆ 𝐵
10 9 a1i ⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
11 6 8 10 1 5 cncfmptssg ⊢ ( 𝜑 → ( 𝑠 ∈ 𝐵 ↦ ( 𝑋 + 𝑠 ) ) ∈ ( 𝐵 –cn→ 𝐴 ) )
12 11 2 cncfcompt ⊢ ( 𝜑 → ( 𝑠 ∈ 𝐵 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( 𝐵 –cn→ ℂ ) )