Theorem esumgsum

Description: A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		esumgsum.1	⊢ Ⅎ 𝑘 𝜑
2		esumgsum.2	⊢ Ⅎ 𝑘 𝐴
3		esumgsum.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		esumgsum.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5		xrge0base	⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
6		xrge00	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
7		xrge0cmn	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
8	7	a1i	⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
9		xrge0tps	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp
10	9	a1i	⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp )
11		nfcv	⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
12		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
13	1 2 11 4 12	fmptdF	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
14	4	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐵 ∈ ( 0 [,] +∞ ) ) )
15	1 14	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
16	2	fnmptf	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
17	15 16	syl	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
18		0xr	⊢ 0 ∈ ℝ*
19	18	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
20	17 3 19	fndmfifsupp	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) finSupp 0 )
21	5 6 8 10 3 13 20	tsmsid	⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
22	1 2 3 4 21	esumid	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )