Theorem fsumcncf

Description: The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fsumcncf.x	$$⊢\phi \to X\subseteq ℂ$$
	fsumcncf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumcncf.cncf	$$⊢\left(\phi \wedge k\in A\right)\to \left(x\in X⟼B\right):X\underset{cn}{⟶}ℂ$$
Assertion	fsumcncf	$$⊢\phi \to \left(x\in X⟼\sum _{k\in A}B\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		fsumcncf.x	$$⊢\phi \to X\subseteq ℂ$$
2		fsumcncf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsumcncf.cncf	$$⊢\left(\phi \wedge k\in A\right)\to \left(x\in X⟼B\right):X\underset{cn}{⟶}ℂ$$
4		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
5	4	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
6	5	a1i	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
7		resttopon	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge X\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\in \mathrm{TopOn}\left(X\right)$$
8	6 1 7	syl2anc	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\in \mathrm{TopOn}\left(X\right)$$
9		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
10		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X$$
11	4	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
12		unicntop	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
13	12	restid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
14	11 13	ax-mp	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
15	14	eqcomi	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
16	4 10 15	cncfcn	$$⊢\left(X\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to X\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
17	1 9 16	syl2anc	$$⊢\phi \to X\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
18	17	adantr	$$⊢\left(\phi \wedge k\in A\right)\to X\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
19	3 18	eleqtrd	$$⊢\left(\phi \wedge k\in A\right)\to \left(x\in X⟼B\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
20	4 8 2 19	fsumcnf	$$⊢\phi \to \left(x\in X⟼\sum _{k\in A}B\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
21	20 17	eleqtrrd	$$⊢\phi \to \left(x\in X⟼\sum _{k\in A}B\right):X\underset{cn}{⟶}ℂ$$