Metamath Proof Explorer


Theorem mulcncf

Description: The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses mulcncf.1 ( 𝜑 → ( 𝑥𝑋𝐴 ) ∈ ( 𝑋cn→ ℂ ) )
mulcncf.2 ( 𝜑 → ( 𝑥𝑋𝐵 ) ∈ ( 𝑋cn→ ℂ ) )
Assertion mulcncf ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝑋cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 mulcncf.1 ( 𝜑 → ( 𝑥𝑋𝐴 ) ∈ ( 𝑋cn→ ℂ ) )
2 mulcncf.2 ( 𝜑 → ( 𝑥𝑋𝐵 ) ∈ ( 𝑋cn→ ℂ ) )
3 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4 3 mulcn · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
5 4 a1i ( 𝜑 → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
6 3 5 1 2 cncfmpt2f ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝑋cn→ ℂ ) )