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

Metamath Proof Explorer

Theorem refsum2cn

Description: The sum of two continuus real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses refsum2cn.1 ⊢ Ⅎ _ x F
refsum2cn.2 ⊢ Ⅎ _ x G
refsum2cn.3 ⊢ Ⅎ x φ
refsum2cn.4 ⊢ K = topGen ⁡ ran ⁡ .
refsum2cn.5 ⊢ φ → J ∈ TopOn ⁡ X
refsum2cn.6 ⊢ φ → F ∈ J Cn K
refsum2cn.7 ⊢ φ → G ∈ J Cn K
Assertion refsum2cn ⊢ φ → x ∈ X ⟼ F ⁡ x + G ⁡ x ∈ J Cn K

Proof

Step Hyp Ref Expression
1 refsum2cn.1 ⊢ Ⅎ _ x F
2 refsum2cn.2 ⊢ Ⅎ _ x G
3 refsum2cn.3 ⊢ Ⅎ x φ
4 refsum2cn.4 ⊢ K = topGen ⁡ ran ⁡ .
5 refsum2cn.5 ⊢ φ → J ∈ TopOn ⁡ X
6 refsum2cn.6 ⊢ φ → F ∈ J Cn K
7 refsum2cn.7 ⊢ φ → G ∈ J Cn K
8 nfcv ⊢ Ⅎ _ x 1 2
9 nfv ⊢ Ⅎ x k = 1
10 9 1 2 nfif ⊢ Ⅎ _ x if k = 1 F G
11 8 10 nfmpt ⊢ Ⅎ _ x k ∈ 1 2 ⟼ if k = 1 F G
12 eqid ⊢ k ∈ 1 2 ⟼ if k = 1 F G = k ∈ 1 2 ⟼ if k = 1 F G
13 11 1 2 3 12 4 5 6 7 refsum2cnlem1 ⊢ φ → x ∈ X ⟼ F ⁡ x + G ⁡ x ∈ J Cn K