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 ⊢ Ⅎ 𝑥 𝐹
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 𝐾 ) )