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→ ℂ ) ) |
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→ ℂ ) ) |