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 𝐾 ) )