Metamath Proof Explorer

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

Proof

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