Theorem mulcncff

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

	Ref	Expression
Hypotheses	mulcncff.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
	mulcncff.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
Assertion	mulcncff	⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		mulcncff.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
2		mulcncff.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
3		cncfrss	⊢ ( 𝐹 ∈ ( 𝑋 –cn→ ℂ ) → 𝑋 ⊆ ℂ )
4		cnex	⊢ ℂ ∈ V
5	4	ssex	⊢ ( 𝑋 ⊆ ℂ → 𝑋 ∈ V )
6	1 3 5	3syl	⊢ ( 𝜑 → 𝑋 ∈ V )
7		cncff	⊢ ( 𝐹 ∈ ( 𝑋 –cn→ ℂ ) → 𝐹 : 𝑋 ⟶ ℂ )
8	1 7	syl	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
9	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
10		cncff	⊢ ( 𝐺 ∈ ( 𝑋 –cn→ ℂ ) → 𝐺 : 𝑋 ⟶ ℂ )
11	2 10	syl	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
12	11	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
13	8	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
14	11	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
15	6 9 12 13 14	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
16	13 1	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
17	14 2	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
18	16 17	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( 𝑋 –cn→ ℂ ) )
19	15 18	eqeltrd	⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )