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 ⊢ φ → A ∈ V
sge0snmpt.c ⊢ φ → C ∈ 0 +∞
sge0snmpt.b ⊢ k = A → B = C
Assertion sge0snmpt ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = C

Proof

Step Hyp Ref Expression
1 sge0snmpt.a ⊢ φ → A ∈ V
2 sge0snmpt.c ⊢ φ → C ∈ 0 +∞
3 sge0snmpt.b ⊢ k = A → B = C
4 elsni ⊢ k ∈ A → k = A
5 4 3 syl ⊢ k ∈ A → B = C
6 5 adantl ⊢ φ ∧ k ∈ A → B = C
7 2 adantr ⊢ φ ∧ k ∈ A → C ∈ 0 +∞
8 6 7 eqeltrd ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
9 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
10 8 9 fmptd ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
11 1 10 sge0sn ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = k ∈ A ⟼ B ⁡ A
12 eqidd ⊢ φ → k ∈ A ⟼ B = k ∈ A ⟼ B
13 3 adantl ⊢ φ ∧ k = A → B = C
14 snidg ⊢ A ∈ V → A ∈ A
15 1 14 syl ⊢ φ → A ∈ A
16 12 13 15 2 fvmptd ⊢ φ → k ∈ A ⟼ B ⁡ A = C
17 11 16 eqtrd ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = C