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	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
	fsumcnf.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	fsumcnf.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumcnf.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	fsumcnf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		fsumcnf.1	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2		fsumcnf.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		fsumcnf.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		fsumcnf.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
5		nfcv	⊢ Ⅎ 𝑦 Σ 𝑘 ∈ 𝐴 𝐵
6		nfcv	⊢ Ⅎ 𝑥 𝐴
7		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
8	6 7	nfsum	⊢ Ⅎ 𝑥 Σ 𝑘 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	9	sumeq2sdv	⊢ ( 𝑥 = 𝑦 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
11	5 8 10	cbvmpt	⊢ ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
12		nfcv	⊢ Ⅎ 𝑦 𝐵
13	12 7 9	cbvmpt	⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
14	13 4	eqeltrrid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
15	1 2 3 14	fsumcn	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )
16	11 15	eqeltrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ( 𝐽 Cn 𝐾 ) )