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		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
9		nfcv	⊢ Ⅎ 𝑘 𝑗
10	8 9	nffv	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 )
11		nfcv	⊢ Ⅎ 𝑗 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 )
12	7 10 11	cbvsum	⊢ Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 )
13	12	a1i	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
15	4	fvmpt2	⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
16	14 3 15	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
17	16	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 ) )
18	1 17	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
19	18	sumeq2d	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 𝐵 )
20	6 13 19	3eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )