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

Metamath Proof Explorer

Theorem fsumcnf

Description: A finite sum of functions to complex numbers from a common topological space is continuous, without disjoint var constraint x ph. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fsumcnf.1 ⊢ K = TopOpen ⁡ ℂ fld
fsumcnf.2 ⊢ φ → J ∈ TopOn ⁡ X
fsumcnf.3 ⊢ φ → A ∈ Fin
fsumcnf.4 ⊢ φ ∧ k ∈ A → x ∈ X ⟼ B ∈ J Cn K
Assertion fsumcnf ⊢ φ → x ∈ X ⟼ ∑ k ∈ A B ∈ J Cn K

Proof

Step Hyp Ref Expression
1 fsumcnf.1 ⊢ K = TopOpen ⁡ ℂ fld
2 fsumcnf.2 ⊢ φ → J ∈ TopOn ⁡ X
3 fsumcnf.3 ⊢ φ → A ∈ Fin
4 fsumcnf.4 ⊢ φ ∧ k ∈ A → x ∈ X ⟼ B ∈ J Cn K
5 nfcv ⊢ Ⅎ _ y ∑ k ∈ A B
6 nfcv ⊢ Ⅎ _ x A
7 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
8 6 7 nfsum ⊢ Ⅎ _ x ∑ k ∈ A ⦋ y / x⦌ B
9 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
10 9 sumeq2sdv ⊢ x = y → ∑ k ∈ A B = ∑ k ∈ A ⦋ y / x⦌ B
11 5 8 10 cbvmpt ⊢ x ∈ X ⟼ ∑ k ∈ A B = y ∈ X ⟼ ∑ k ∈ A ⦋ y / x⦌ B
12 nfcv ⊢ Ⅎ _ y B
13 12 7 9 cbvmpt ⊢ x ∈ X ⟼ B = y ∈ X ⟼ ⦋ y / x⦌ B
14 13 4 eqeltrrid ⊢ φ ∧ k ∈ A → y ∈ X ⟼ ⦋ y / x⦌ B ∈ J Cn K
15 1 2 3 14 fsumcn ⊢ φ → y ∈ X ⟼ ∑ k ∈ A ⦋ y / x⦌ B ∈ J Cn K
16 11 15 eqeltrid ⊢ φ → x ∈ X ⟼ ∑ k ∈ A B ∈ J Cn K