Theorem sge0snmpt

Description: A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0snmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0snmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,] +∞ ) )
	sge0snmpt.b	⊢ ( 𝑘 = 𝐴 → 𝐵 = 𝐶 )
Assertion	sge0snmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		sge0snmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		sge0snmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,] +∞ ) )
3		sge0snmpt.b	⊢ ( 𝑘 = 𝐴 → 𝐵 = 𝐶 )
4		elsni	⊢ ( 𝑘 ∈ { 𝐴 } → 𝑘 = 𝐴 )
5	4 3	syl	⊢ ( 𝑘 ∈ { 𝐴 } → 𝐵 = 𝐶 )
6	5	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 } ) → 𝐵 = 𝐶 )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 } ) → 𝐶 ∈ ( 0 [,] +∞ ) )
8	6 7	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 } ) → 𝐵 ∈ ( 0 [,] +∞ ) )
9		eqid	⊢ ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) = ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 )
10	8 9	fmptd	⊢ ( 𝜑 → ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) : { 𝐴 } ⟶ ( 0 [,] +∞ ) )
11	1 10	sge0sn	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) ) = ( ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) ‘ 𝐴 ) )
12		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) = ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) )
13	3	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐵 = 𝐶 )
14		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
15	1 14	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
16	12 13 15 2	fvmptd	⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 )
17	11 16	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) ) = 𝐶 )