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	⊢ Ⅎ 𝑥 𝐹
	refsum2cn.2	⊢ Ⅎ 𝑥 𝐺
	refsum2cn.3	⊢ Ⅎ 𝑥 𝜑
	refsum2cn.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
	refsum2cn.5	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	refsum2cn.6	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
	refsum2cn.7	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	refsum2cn	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		refsum2cn.1	⊢ Ⅎ 𝑥 𝐹
2		refsum2cn.2	⊢ Ⅎ 𝑥 𝐺
3		refsum2cn.3	⊢ Ⅎ 𝑥 𝜑
4		refsum2cn.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
5		refsum2cn.5	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6		refsum2cn.6	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7		refsum2cn.7	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
8		nfcv	⊢ Ⅎ 𝑥 { 1 , 2 }
9		nfv	⊢ Ⅎ 𝑥 𝑘 = 1
10	9 1 2	nfif	⊢ Ⅎ 𝑥 if ( 𝑘 = 1 , 𝐹 , 𝐺 )
11	8 10	nfmpt	⊢ Ⅎ 𝑥 ( 𝑘 ∈ { 1 , 2 } ↦ if ( 𝑘 = 1 , 𝐹 , 𝐺 ) )
12		eqid	⊢ ( 𝑘 ∈ { 1 , 2 } ↦ if ( 𝑘 = 1 , 𝐹 , 𝐺 ) ) = ( 𝑘 ∈ { 1 , 2 } ↦ if ( 𝑘 = 1 , 𝐹 , 𝐺 ) )
13	11 1 2 3 12 4 5 6 7	refsum2cnlem1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐾 ) )