Theorem sge0fsummptf

Description: The generalized 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, 21-Nov-2020)

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

Proof

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