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	|- F/_ x F
	refsum2cn.2	|- F/_ x G
	refsum2cn.3	|- F/ x ph
	refsum2cn.4	|- K = ( topGen ` ran (,) )
	refsum2cn.5	|- ( ph -> J e. ( TopOn ` X ) )
	refsum2cn.6	|- ( ph -> F e. ( J Cn K ) )
	refsum2cn.7	|- ( ph -> G e. ( J Cn K ) )
Assertion	refsum2cn	|- ( ph -> ( x e. X |-> ( ( F ` x ) + ( G ` x ) ) ) e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		refsum2cn.1	|- F/_ x F
2		refsum2cn.2	|- F/_ x G
3		refsum2cn.3	|- F/ x ph
4		refsum2cn.4	|- K = ( topGen ` ran (,) )
5		refsum2cn.5	|- ( ph -> J e. ( TopOn ` X ) )
6		refsum2cn.6	|- ( ph -> F e. ( J Cn K ) )
7		refsum2cn.7	|- ( ph -> G e. ( J Cn K ) )
8		nfcv	|- F/_ x { 1 , 2 }
9		nfv	|- F/ x k = 1
10	9 1 2	nfif	|- F/_ x if ( k = 1 , F , G )
11	8 10	nfmpt	|- F/_ x ( k e. { 1 , 2 } |-> if ( k = 1 , F , G ) )
12		eqid	|- ( k e. { 1 , 2 } |-> if ( k = 1 , F , G ) ) = ( k e. { 1 , 2 } |-> if ( k = 1 , F , G ) )
13	11 1 2 3 12 4 5 6 7	refsum2cnlem1	|- ( ph -> ( x e. X |-> ( ( F ` x ) + ( G ` x ) ) ) e. ( J Cn K ) )