Metamath Proof Explorer


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 ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ { 𝐴 } ↦ 𝐵 ) ) = 𝐶 )