Theorem esumel

Description: The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017)

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

Proof

Step	Hyp	Ref	Expression
1		esumel.1	⊢ Ⅎ 𝑘 𝜑
2		esumel.2	⊢ Ⅎ 𝑘 𝐴
3		esumel.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		esumel.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5	4	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐵 ∈ ( 0 [,] +∞ ) ) )
6	1 5	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
7	2	esumcl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
8	3 6 7	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
9		snidg	⊢ ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ { Σ* 𝑘 ∈ 𝐴 𝐵 } )
10	8 9	syl	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ { Σ* 𝑘 ∈ 𝐴 𝐵 } )
11		eqid	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
12		nfcv	⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
13		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
14	1 2 12 4 13	fmptdf2	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
15		inss1	⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
16		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
17	15 16	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ 𝒫 𝐴 )
18	17	elpwid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ⊆ 𝐴 )
19		nfcv	⊢ Ⅎ 𝑘 𝑥
20	2 19	resmptf	⊢ ( 𝑥 ⊆ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) = ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) )
21	18 20	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) = ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) )
22	21	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) )
23	22	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) )
24	1 2 3 4 23	esumval	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) , ℝ* , < ) )
25	11 3 14 24	xrge0tsmsd	⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = { Σ* 𝑘 ∈ 𝐴 𝐵 } )
26	10 25	eleqtrrd	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )