Metamath Proof Explorer

Theorem fsumcncf

Description: The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fsumcncf.x ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
fsumcncf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumcncf.cncf ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion fsumcncf ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 fsumcncf.x ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
2 fsumcncf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fsumcncf.cncf ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
4 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
5 4 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
6 5 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
7 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
8 6 1 7 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
9 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
10 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 )
11 4 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
12 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
13 12 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
14 11 13 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
15 14 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
16 4 10 15 cncfcn ⊢ ( ( 𝑋 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
17 1 9 16 syl2anc ⊢ ( 𝜑 → ( 𝑋 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑋 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
19 3 18 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
20 4 8 2 19 fsumcnf ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) )
21 20 17 eleqtrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )