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

Metamath Proof Explorer

Theorem subcncf

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

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

Proof

Step Hyp Ref Expression
1 subcncf.a ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
2 subcncf.b ⊢ φ → x ∈ X ⟼ B : X ⟶cn ℂ
3 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
4 3 subcn ⊢ − ∈ 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 ℂ