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	$$⊢\underset{\_}{Ⅎ}xF$$
	refsum2cn.2	$$⊢\underset{\_}{Ⅎ}xG$$
	refsum2cn.3	$$⊢Ⅎx\phi$$
	refsum2cn.4	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	refsum2cn.5	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	refsum2cn.6	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
	refsum2cn.7	$$⊢\phi \to G\in \left(J\mathrm{Cn}K\right)$$
Assertion	refsum2cn	$$⊢\phi \to \left(x\in X⟼F\left(x\right)+G\left(x\right)\right)\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		refsum2cn.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		refsum2cn.2	$$⊢\underset{\_}{Ⅎ}xG$$
3		refsum2cn.3	$$⊢Ⅎx\phi$$
4		refsum2cn.4	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
5		refsum2cn.5	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
6		refsum2cn.6	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
7		refsum2cn.7	$$⊢\phi \to G\in \left(J\mathrm{Cn}K\right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{1,2\right\}$$
9		nfv	$$⊢Ⅎxk=1$$
10	9 1 2	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(k=1,F,G\right)$$
11	8 10	nfmpt	$$⊢\underset{\_}{Ⅎ}x\left(k\in \left\{1,2\right\}⟼if\left(k=1,F,G\right)\right)$$
12		eqid	$$⊢\left(k\in \left\{1,2\right\}⟼if\left(k=1,F,G\right)\right)=\left(k\in \left\{1,2\right\}⟼if\left(k=1,F,G\right)\right)$$
13	11 1 2 3 12 4 5 6 7	refsum2cnlem1	$$⊢\phi \to \left(x\in X⟼F\left(x\right)+G\left(x\right)\right)\in \left(J\mathrm{Cn}K\right)$$