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 φ X
fsumcncf.a φ A Fin
fsumcncf.cncf φ k A x X B : X cn
Assertion fsumcncf φ x X k A B : X cn

Proof

Step Hyp Ref Expression
1 fsumcncf.x φ X
2 fsumcncf.a φ A Fin
3 fsumcncf.cncf φ k A x X B : X cn
4 eqid TopOpen fld = TopOpen fld
5 4 cnfldtopon TopOpen fld TopOn
6 5 a1i φ TopOpen fld TopOn
7 resttopon TopOpen fld TopOn X TopOpen fld 𝑡 X TopOn X
8 6 1 7 syl2anc φ TopOpen fld 𝑡 X TopOn X
9 ssidd φ
10 eqid TopOpen fld 𝑡 X = TopOpen fld 𝑡 X
11 4 cnfldtop TopOpen fld Top
12 unicntop = TopOpen fld
13 12 restid TopOpen fld Top TopOpen fld 𝑡 = TopOpen fld
14 11 13 ax-mp TopOpen fld 𝑡 = TopOpen fld
15 14 eqcomi TopOpen fld = TopOpen fld 𝑡
16 4 10 15 cncfcn X X cn = TopOpen fld 𝑡 X Cn TopOpen fld
17 1 9 16 syl2anc φ X cn = TopOpen fld 𝑡 X Cn TopOpen fld
18 17 adantr φ k A X cn = TopOpen fld 𝑡 X Cn TopOpen fld
19 3 18 eleqtrd φ k A x X B TopOpen fld 𝑡 X Cn TopOpen fld
20 4 8 2 19 fsumcnf φ x X k A B TopOpen fld 𝑡 X Cn TopOpen fld
21 20 17 eleqtrrd φ x X k A B : X cn