Theorem fsumcnf

Description: A finite sum of functions to complex numbers from a common topological space is continuous, without disjoint var constraint x ph. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	fsumcnf.1	|- K = ( TopOpen ` CCfld )
	fsumcnf.2	|- ( ph -> J e. ( TopOn ` X ) )
	fsumcnf.3	|- ( ph -> A e. Fin )
	fsumcnf.4	|- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
Assertion	fsumcnf	|- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		fsumcnf.1	|- K = ( TopOpen ` CCfld )
2		fsumcnf.2	|- ( ph -> J e. ( TopOn ` X ) )
3		fsumcnf.3	|- ( ph -> A e. Fin )
4		fsumcnf.4	|- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )
5		nfcv	|- F/_ y sum_ k e. A B
6		nfcv	|- F/_ x A
7		nfcsb1v	|- F/_ x [_ y / x ]_ B
8	6 7	nfsum	|- F/_ x sum_ k e. A [_ y / x ]_ B
9		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
10	9	sumeq2sdv	|- ( x = y -> sum_ k e. A B = sum_ k e. A [_ y / x ]_ B )
11	5 8 10	cbvmpt	|- ( x e. X |-> sum_ k e. A B ) = ( y e. X |-> sum_ k e. A [_ y / x ]_ B )
12		nfcv	|- F/_ y B
13	12 7 9	cbvmpt	|- ( x e. X |-> B ) = ( y e. X |-> [_ y / x ]_ B )
14	13 4	eqeltrrid	|- ( ( ph /\ k e. A ) -> ( y e. X |-> [_ y / x ]_ B ) e. ( J Cn K ) )
15	1 2 3 14	fsumcn	|- ( ph -> ( y e. X |-> sum_ k e. A [_ y / x ]_ B ) e. ( J Cn K ) )
16	11 15	eqeltrid	|- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )