Metamath Proof Explorer


Theorem 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 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 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
5 cncfrss ( ( 𝑥𝑋𝐴 ) ∈ ( 𝑋cn→ ℂ ) → 𝑋 ⊆ ℂ )
6 1 5 syl ( 𝜑𝑋 ⊆ ℂ )
7 resttopon ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
8 4 6 7 sylancr ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
9 ssid ℂ ⊆ ℂ
10 eqid ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 )
11 4 toponrestid ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
12 3 10 11 cncfcn ( ( 𝑋 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
13 6 9 12 sylancl ( 𝜑 → ( 𝑋cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
14 1 13 eleqtrd ( 𝜑 → ( 𝑥𝑋𝐴 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
15 2 13 eleqtrd ( 𝜑 → ( 𝑥𝑋𝐵 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
16 4 a1i ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
17 3 mpomulcn ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
18 17 a1i ( 𝜑 → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
19 oveq12 ( ( 𝑢 = 𝐴𝑣 = 𝐵 ) → ( 𝑢 · 𝑣 ) = ( 𝐴 · 𝐵 ) )
20 8 14 15 16 16 18 19 cnmpt12 ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
21 20 13 eleqtrrd ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝑋cn→ ℂ ) )