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

Metamath Proof Explorer

Theorem fsumcnf

Proof