This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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