Theorem mulcncff

Description: The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	mulcncff.f	$$⊢\phi \to F:X\underset{cn}{⟶}ℂ$$
	mulcncff.g	$$⊢\phi \to G:X\underset{cn}{⟶}ℂ$$
Assertion	mulcncff	$$⊢\phi \to \left(F{\times }_{f}G\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		mulcncff.f	$$⊢\phi \to F:X\underset{cn}{⟶}ℂ$$
2		mulcncff.g	$$⊢\phi \to G:X\underset{cn}{⟶}ℂ$$
3		cncfrss	$$⊢F:X\underset{cn}{⟶}ℂ\to X\subseteq ℂ$$
4		cnex	$$⊢ℂ\in \mathrm{V}$$
5	4	ssex	$$⊢X\subseteq ℂ\to X\in \mathrm{V}$$
6	1 3 5	3syl	$$⊢\phi \to X\in \mathrm{V}$$
7		cncff	$$⊢F:X\underset{cn}{⟶}ℂ\to F:X⟶ℂ$$
8	1 7	syl	$$⊢\phi \to F:X⟶ℂ$$
9	8	ffvelrnda	$$⊢\left(\phi \wedge x\in X\right)\to F\left(x\right)\in ℂ$$
10		cncff	$$⊢G:X\underset{cn}{⟶}ℂ\to G:X⟶ℂ$$
11	2 10	syl	$$⊢\phi \to G:X⟶ℂ$$
12	11	ffvelrnda	$$⊢\left(\phi \wedge x\in X\right)\to G\left(x\right)\in ℂ$$
13	8	feqmptd	$$⊢\phi \to F=\left(x\in X⟼F\left(x\right)\right)$$
14	11	feqmptd	$$⊢\phi \to G=\left(x\in X⟼G\left(x\right)\right)$$
15	6 9 12 13 14	offval2	$$⊢\phi \to F{\times }_{f}G=\left(x\in X⟼F\left(x\right)G\left(x\right)\right)$$
16	13 1	eqeltrrd	$$⊢\phi \to \left(x\in X⟼F\left(x\right)\right):X\underset{cn}{⟶}ℂ$$
17	14 2	eqeltrrd	$$⊢\phi \to \left(x\in X⟼G\left(x\right)\right):X\underset{cn}{⟶}ℂ$$
18	16 17	mulcncf	$$⊢\phi \to \left(x\in X⟼F\left(x\right)G\left(x\right)\right):X\underset{cn}{⟶}ℂ$$
19	15 18	eqeltrd	$$⊢\phi \to \left(F{\times }_{f}G\right):X\underset{cn}{⟶}ℂ$$