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=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	fsumcnf.2	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	fsumcnf.3	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumcnf.4	$$⊢\left(\phi \wedge k\in A\right)\to \left(x\in X⟼B\right)\in \left(J\mathrm{Cn}K\right)$$
Assertion	fsumcnf	$$⊢\phi \to \left(x\in X⟼\sum _{k\in A}B\right)\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsumcnf.1	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		fsumcnf.2	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
3		fsumcnf.3	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fsumcnf.4	$$⊢\left(\phi \wedge k\in A\right)\to \left(x\in X⟼B\right)\in \left(J\mathrm{Cn}K\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}y\sum _{k\in A}B$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
7		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
8	6 7	nfsum	$$⊢\underset{\_}{Ⅎ}x\sum _{k\in A}⦋y/x⦌B$$
9		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
10	9	sumeq2sdv	$$⊢x=y\to \sum _{k\in A}B=\sum _{k\in A}⦋y/x⦌B$$
11	5 8 10	cbvmpt	$$⊢\left(x\in X⟼\sum _{k\in A}B\right)=\left(y\in X⟼\sum _{k\in A}⦋y/x⦌B\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
13	12 7 9	cbvmpt	$$⊢\left(x\in X⟼B\right)=\left(y\in X⟼⦋y/x⦌B\right)$$
14	13 4	eqeltrrid	$$⊢\left(\phi \wedge k\in A\right)\to \left(y\in X⟼⦋y/x⦌B\right)\in \left(J\mathrm{Cn}K\right)$$
15	1 2 3 14	fsumcn	$$⊢\phi \to \left(y\in X⟼\sum _{k\in A}⦋y/x⦌B\right)\in \left(J\mathrm{Cn}K\right)$$
16	11 15	eqeltrid	$$⊢\phi \to \left(x\in X⟼\sum _{k\in A}B\right)\in \left(J\mathrm{Cn}K\right)$$