Theorem sge0snmptf

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

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

Proof

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