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

Metamath Proof Explorer

Theorem addcncff

Description: The sum of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses addcncff.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
addcncff.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
Assertion addcncff ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 addcncff.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
2 addcncff.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
3 cncfrss ⊢ ( 𝐹 ∈ ( 𝑋 –cn→ ℂ ) → 𝑋 ⊆ ℂ )
4 cnex ⊢ ℂ ∈ V
5 4 ssex ⊢ ( 𝑋 ⊆ ℂ → 𝑋 ∈ V )
6 1 3 5 3syl ⊢ ( 𝜑 → 𝑋 ∈ V )
7 cncff ⊢ ( 𝐹 ∈ ( 𝑋 –cn→ ℂ ) → 𝐹 : 𝑋 ⟶ ℂ )
8 1 7 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
9 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
10 cncff ⊢ ( 𝐺 ∈ ( 𝑋 –cn→ ℂ ) → 𝐺 : 𝑋 ⟶ ℂ )
11 2 10 syl ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
12 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
13 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
14 11 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
15 6 9 12 13 14 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
16 13 1 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
17 14 2 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
18 16 17 addcncf ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
19 15 18 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )