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

Metamath Proof Explorer

Theorem addcncf

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

Ref Expression
Hypotheses addcncf.a ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
addcncf.b ⊢ φ → x ∈ X ⟼ B : X ⟶cn ℂ
Assertion addcncf ⊢ φ → x ∈ X ⟼ A + B : X ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 addcncf.a ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
2 addcncf.b ⊢ φ → x ∈ X ⟼ B : X ⟶cn ℂ
3 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
4 3 addcn ⊢ + ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
5 4 a1i ⊢ φ → + ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
6 3 5 1 2 cncfmpt2f ⊢ φ → x ∈ X ⟼ A + B : X ⟶cn ℂ