Theorem sge0fsummpt

Description: The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0fsummpt.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	sge0fsummpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion	sge0fsummpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sge0fsummpt.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		sge0fsummpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
3		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
4	2 3	fmptd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
5	1 4	sge0fsum	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) )
6		fveq2	⊢ ( 𝑗 = 𝑘 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) )
7		nfcv	⊢ Ⅎ 𝑘 𝐴
8		nfcv	⊢ Ⅎ 𝑗 𝐴
9		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
10		nfcv	⊢ Ⅎ 𝑘 𝑗
11	9 10	nffv	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 )
12		nfcv	⊢ Ⅎ 𝑗 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 )
13	6 7 8 11 12	cbvsum	⊢ Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 )
14	13	a1i	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
16	3	fvmpt2	⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
17	15 2 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
18	17	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 𝐵 )
19	5 14 18	3eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )