# Metamath Proof Explorer

## Theorem refsumcn

Description: A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses refsumcn.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
refsumcn.2 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
refsumcn.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
refsumcn.4 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
refsumcn.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$
Assertion refsumcn ${⊢}{\phi }\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$

### Proof

Step Hyp Ref Expression
1 refsumcn.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 refsumcn.2 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
3 refsumcn.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
4 refsumcn.4 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
5 refsumcn.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$
6 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
7 6 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
8 2 7 eqtri ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
9 8 oveq2i ${⊢}{J}\mathrm{Cn}{K}={J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
10 5 9 eleqtrdi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)$
11 6 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
12 11 a1i ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
13 3 adantr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
14 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
15 2 14 eqeltri ${⊢}{K}\in \mathrm{TopOn}\left(ℝ\right)$
16 15 a1i ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {K}\in \mathrm{TopOn}\left(ℝ\right)$
17 cnf2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left(ℝ\right)\wedge \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}{K}\right)\right)\to \left({x}\in {X}⟼{B}\right):{X}⟶ℝ$
18 13 16 5 17 syl3anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right):{X}⟶ℝ$
19 18 frnd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \mathrm{ran}\left({x}\in {X}⟼{B}\right)\subseteq ℝ$
20 ax-resscn ${⊢}ℝ\subseteq ℂ$
21 20 a1i ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to ℝ\subseteq ℂ$
22 cnrest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({x}\in {X}⟼{B}\right)\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left(\left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
23 12 19 21 22 syl3anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left(\left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
24 10 23 mpbird ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}⟼{B}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
25 6 3 4 24 fsumcnf ${⊢}{\phi }\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
26 11 a1i ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
27 4 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in \mathrm{Fin}$
28 simpll ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to {\phi }$
29 simpr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to {k}\in {A}$
30 28 29 jca ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to \left({\phi }\wedge {k}\in {A}\right)$
31 simplr ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to {x}\in {X}$
32 eqid ${⊢}\left({x}\in {X}⟼{B}\right)=\left({x}\in {X}⟼{B}\right)$
33 32 fmpt ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in ℝ↔\left({x}\in {X}⟼{B}\right):{X}⟶ℝ$
34 18 33 sylibr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in ℝ$
35 rsp ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{B}\in ℝ\to \left({x}\in {X}\to {B}\in ℝ\right)$
36 34 35 syl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({x}\in {X}\to {B}\in ℝ\right)$
37 30 31 36 sylc ${⊢}\left(\left({\phi }\wedge {x}\in {X}\right)\wedge {k}\in {A}\right)\to {B}\in ℝ$
38 27 37 fsumrecl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \sum _{{k}\in {A}}{B}\in ℝ$
39 38 ex ${⊢}{\phi }\to \left({x}\in {X}\to \sum _{{k}\in {A}}{B}\in ℝ\right)$
40 1 39 ralrimi ${⊢}{\phi }\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {A}}{B}\in ℝ$
41 eqid ${⊢}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)=\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)$
42 41 fnmpt ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {A}}{B}\in ℝ\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)Fn{X}$
43 40 42 syl ${⊢}{\phi }\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)Fn{X}$
44 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{X}$
45 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
46 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)$
47 44 45 46 fvelrnbf ${⊢}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)Fn{X}\to \left({y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)$
48 43 47 syl ${⊢}{\phi }\to \left({y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)$
49 48 biimpa ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}$
50 46 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)$
51 50 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)$
52 1 51 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\right)$
53 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}ℝ$
54 53 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in ℝ$
55 simpr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}\in {X}$
56 55 38 jca ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({x}\in {X}\wedge \sum _{{k}\in {A}}{B}\in ℝ\right)$
57 41 fvmpt2 ${⊢}\left({x}\in {X}\wedge \sum _{{k}\in {A}}{B}\in ℝ\right)\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)=\sum _{{k}\in {A}}{B}$
58 56 57 syl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)=\sum _{{k}\in {A}}{B}$
59 58 3adant3 ${⊢}\left({\phi }\wedge {x}\in {X}\wedge \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)=\sum _{{k}\in {A}}{B}$
60 simp3 ${⊢}\left({\phi }\wedge {x}\in {X}\wedge \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}$
61 59 60 eqtr3d ${⊢}\left({\phi }\wedge {x}\in {X}\wedge \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)\to \sum _{{k}\in {A}}{B}={y}$
62 38 3adant3 ${⊢}\left({\phi }\wedge {x}\in {X}\wedge \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)\to \sum _{{k}\in {A}}{B}\in ℝ$
63 61 62 eqeltrrd ${⊢}\left({\phi }\wedge {x}\in {X}\wedge \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)\to {y}\in ℝ$
64 63 3adant1r ${⊢}\left(\left({\phi }\wedge {y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\right)\wedge {x}\in {X}\wedge \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\right)\to {y}\in ℝ$
65 64 3exp ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\right)\to \left({x}\in {X}\to \left(\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\to {y}\in ℝ\right)\right)$
66 52 54 65 rexlimd ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\right)\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\left({x}\right)={y}\to {y}\in ℝ\right)$
67 49 66 mpd ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\right)\to {y}\in ℝ$
68 67 ex ${⊢}{\phi }\to \left({y}\in \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\to {y}\in ℝ\right)$
69 68 ssrdv ${⊢}{\phi }\to \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\subseteq ℝ$
70 20 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
71 cnrest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left(\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
72 26 69 70 71 syl3anc ${⊢}{\phi }\to \left(\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
73 25 72 mpbid ${⊢}{\phi }\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)$
74 73 9 eleqtrrdi ${⊢}{\phi }\to \left({x}\in {X}⟼\sum _{{k}\in {A}}{B}\right)\in \left({J}\mathrm{Cn}{K}\right)$