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

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 ⊢ Ⅎ 𝑥 𝜑
refsumcn.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
refsumcn.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
refsumcn.4 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
refsumcn.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion refsumcn ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 refsumcn.1 ⊢ Ⅎ 𝑥 𝜑
2 refsumcn.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
3 refsumcn.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 refsumcn.4 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 refsumcn.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
6 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
7 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
8 2 7 eqtri ⊢ 𝐾 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
9 8 oveq2i ⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
10 5 9 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
11 6 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
15 2 14 eqeltri ⊢ 𝐾 ∈ ( TopOn ‘ ℝ )
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐾 ∈ ( TopOn ‘ ℝ ) )
17 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℝ )
18 13 16 5 17 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℝ )
19 18 frnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ran ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ⊆ ℝ )
20 ax-resscn ⊢ ℝ ⊆ ℂ
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ℝ ⊆ ℂ )
22 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
23 12 19 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
24 10 23 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
25 6 3 4 24 fsumcnf ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
26 11 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
27 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ Fin )
28 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝜑 )
29 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
30 28 29 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝑥 ∈ 𝑋 )
32 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
33 32 fmpt ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℝ ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℝ )
34 18 33 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℝ )
35 rsp ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ ℝ → ( 𝑥 ∈ 𝑋 → 𝐵 ∈ ℝ ) )
36 34 35 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 → 𝐵 ∈ ℝ ) )
37 30 31 36 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
38 27 37 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
39 38 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ ) )
40 1 39 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
41 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 )
42 41 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝑋 Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) Fn 𝑋 )
43 40 42 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) Fn 𝑋 )
44 nfcv ⊢ Ⅎ 𝑥 𝑋
45 nfcv ⊢ Ⅎ 𝑥 𝑦
46 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 )
47 44 45 46 fvelrnbf ⊢ ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) Fn 𝑋 → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) )
48 43 47 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) )
49 48 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ) → ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 )
50 46 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 )
51 50 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 )
52 1 51 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) )
53 nfcv ⊢ Ⅎ 𝑥 ℝ
54 53 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ℝ
55 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
56 55 38 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ∧ Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ ) )
57 41 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ ) → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = Σ 𝑘 ∈ 𝐴 𝐵 )
58 56 57 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = Σ 𝑘 ∈ 𝐴 𝐵 )
59 58 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = Σ 𝑘 ∈ 𝐴 𝐵 )
60 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 )
61 59 60 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) → Σ 𝑘 ∈ 𝐴 𝐵 = 𝑦 )
62 38 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
63 61 62 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ ℝ )
64 63 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ ℝ )
65 64 3exp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ) → ( 𝑥 ∈ 𝑋 → ( ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ ℝ ) ) )
66 52 54 65 rexlimd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ ℝ ) )
67 49 66 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ) → 𝑦 ∈ ℝ )
68 67 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) → 𝑦 ∈ ℝ ) )
69 68 ssrdv ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ⊆ ℝ )
70 20 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
71 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
72 26 69 70 71 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
73 25 72 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
74 73 9 eleqtrrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )