Theorem esumid

Description: Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017)

	Ref	Expression
Hypotheses	esumid.p	⊢ Ⅎ 𝑘 𝜑
	esumid.0	⊢ Ⅎ 𝑘 𝐴
	esumid.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumid.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	esumid.3	⊢ ( 𝜑 → 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
Assertion	esumid	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		esumid.p	⊢ Ⅎ 𝑘 𝜑
2		esumid.0	⊢ Ⅎ 𝑘 𝐴
3		esumid.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		esumid.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5		esumid.3	⊢ ( 𝜑 → 𝐶 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
6		df-esum	⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
7		eqid	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
8		nfcv	⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
9		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
10	1 2 8 4 9	fmptdf2	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
11	7 3 10 5	xrge0tsmseq	⊢ ( 𝜑 → 𝐶 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
12	6 11	eqtr4id	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = 𝐶 )