Metamath Proof Explorer


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 ffvelrnda ( ( 𝜑𝑥𝑋 ) → ( 𝐹𝑥 ) ∈ ℂ )
10 cncff ( 𝐺 ∈ ( 𝑋cn→ ℂ ) → 𝐺 : 𝑋 ⟶ ℂ )
11 2 10 syl ( 𝜑𝐺 : 𝑋 ⟶ ℂ )
12 11 ffvelrnda ( ( 𝜑𝑥𝑋 ) → ( 𝐺𝑥 ) ∈ ℂ )
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→ ℂ ) )