Theorem fprodadd2cncf

Description: F is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	fprodadd2cncf.k	$$⊢Ⅎk\phi$$
	fprodadd2cncf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprodadd2cncf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
	fprodadd2cncf.f	$$⊢F=\left(x\in ℂ⟼\prod _{k\in A}\left(B+x\right)\right)$$
Assertion	fprodadd2cncf	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		fprodadd2cncf.k	$$⊢Ⅎk\phi$$
2		fprodadd2cncf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fprodadd2cncf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
4		fprodadd2cncf.f	$$⊢F=\left(x\in ℂ⟼\prod _{k\in A}\left(B+x\right)\right)$$
5	4	a1i	$$⊢\phi \to F=\left(x\in ℂ⟼\prod _{k\in A}\left(B+x\right)\right)$$
6		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
7	6	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
8	7	a1i	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
9		eqid	$$⊢\left(x\in ℂ⟼B+x\right)=\left(x\in ℂ⟼B+x\right)$$
10	3 9	add2cncf	$$⊢\left(\phi \wedge k\in A\right)\to \left(x\in ℂ⟼B+x\right):ℂ\underset{cn}{⟶}ℂ$$
11	6	cncfcn1	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
12	11	a1i	$$⊢\left(\phi \wedge k\in A\right)\to ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
13	10 12	eleqtrd	$$⊢\left(\phi \wedge k\in A\right)\to \left(x\in ℂ⟼B+x\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
14	1 6 8 2 13	fprodcn	$$⊢\phi \to \left(x\in ℂ⟼\prod _{k\in A}\left(B+x\right)\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
15	5 14	eqeltrd	$$⊢\phi \to F\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
16	11	a1i	$$⊢\phi \to ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
17	16	eqcomd	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=ℂ\underset{cn}{⟶}ℂ$$
18	15 17	eleqtrd	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$