Theorem gg-mulcncf

Description: The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	gg-mulcncf.1	$$⊢\phi \to \left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ$$
	gg-mulcncf.2	$$⊢\phi \to \left(x\in X⟼B\right):X\underset{cn}{⟶}ℂ$$
Assertion	gg-mulcncf	$$⊢\phi \to \left(x\in X⟼AB\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		gg-mulcncf.1	$$⊢\phi \to \left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ$$
2		gg-mulcncf.2	$$⊢\phi \to \left(x\in X⟼B\right):X\underset{cn}{⟶}ℂ$$
3		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	3	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
5		cncfrss	$$⊢\left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ\to X\subseteq ℂ$$
6	1 5	syl	$$⊢\phi \to X\subseteq ℂ$$
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	4 6 7	sylancr	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\in \mathrm{TopOn}\left(X\right)$$
9		ssid	$$⊢ℂ\subseteq ℂ$$
10		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X$$
11	4	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
12	3 10 11	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)$$
13	6 9 12	sylancl	$$⊢\phi \to X\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
14	1 13	eleqtrd	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
15	2 13	eleqtrd	$$⊢\phi \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)$$
16	4	a1i	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
17	3	mpomulcn	$$⊢\left(u\in ℂ,v\in ℂ⟼uv\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
18	17	a1i	$$⊢\phi \to \left(u\in ℂ,v\in ℂ⟼uv\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
19		oveq12	$$⊢\left(u=A\wedge v=B\right)\to uv=AB$$
20	8 14 15 16 16 18 19	cnmpt12	$$⊢\phi \to \left(x\in X⟼AB\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
21	20 13	eleqtrrd	$$⊢\phi \to \left(x\in X⟼AB\right):X\underset{cn}{⟶}ℂ$$