Metamath Proof Explorer

Theorem sge0val

Description: The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion sge0val ⊢X∈V∧F:X⟶0+∞→sum^⁡F=if+∞∈ran⁡F+∞supran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡wℝ*<

Proof

Step Hyp Ref Expression
1 df-sumge0 ⊢sum^=x∈V⟼if+∞∈ran⁡x+∞supran⁡y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡wℝ*<
2 1 a1i ⊢X∈V∧F:X⟶0+∞→sum^=x∈V⟼if+∞∈ran⁡x+∞supran⁡y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡wℝ*<
3 rneq ⊢x=F→ran⁡x=ran⁡F
4 3 eleq2d ⊢x=F→+∞∈ran⁡x↔+∞∈ran⁡F
5 4 adantl ⊢X∈V∧F:X⟶0+∞∧x=F→+∞∈ran⁡x↔+∞∈ran⁡F
6 dmeq ⊢x=F→dom⁡x=dom⁡F
7 6 adantl ⊢F:X⟶0+∞∧x=F→dom⁡x=dom⁡F
8 fdm ⊢F:X⟶0+∞→dom⁡F=X
9 8 adantr ⊢F:X⟶0+∞∧x=F→dom⁡F=X
10 7 9 eqtrd ⊢F:X⟶0+∞∧x=F→dom⁡x=X
11 10 pweqd ⊢F:X⟶0+∞∧x=F→𝒫dom⁡x=𝒫X
12 11 ineq1d ⊢F:X⟶0+∞∧x=F→𝒫dom⁡x∩Fin=𝒫X∩Fin
13 12 mpteq1d ⊢F:X⟶0+∞∧x=F→y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡w=y∈𝒫X∩Fin⟼∑w∈yx⁡w
14 13 adantll ⊢X∈V∧F:X⟶0+∞∧x=F→y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡w=y∈𝒫X∩Fin⟼∑w∈yx⁡w
15 fveq1 ⊢x=F→x⁡w=F⁡w
16 15 sumeq2sdv ⊢x=F→∑w∈yx⁡w=∑w∈yF⁡w
17 16 mpteq2dv ⊢x=F→y∈𝒫X∩Fin⟼∑w∈yx⁡w=y∈𝒫X∩Fin⟼∑w∈yF⁡w
18 17 adantl ⊢X∈V∧F:X⟶0+∞∧x=F→y∈𝒫X∩Fin⟼∑w∈yx⁡w=y∈𝒫X∩Fin⟼∑w∈yF⁡w
19 14 18 eqtrd ⊢X∈V∧F:X⟶0+∞∧x=F→y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡w=y∈𝒫X∩Fin⟼∑w∈yF⁡w
20 19 rneqd ⊢X∈V∧F:X⟶0+∞∧x=F→ran⁡y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡w=ran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡w
21 20 supeq1d ⊢X∈V∧F:X⟶0+∞∧x=F→supran⁡y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡wℝ*<=supran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡wℝ*<
22 5 21 ifbieq2d ⊢X∈V∧F:X⟶0+∞∧x=F→if+∞∈ran⁡x+∞supran⁡y∈𝒫dom⁡x∩Fin⟼∑w∈yx⁡wℝ*<=if+∞∈ran⁡F+∞supran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡wℝ*<
23 simpr ⊢X∈V∧F:X⟶0+∞→F:X⟶0+∞
24 simpl ⊢X∈V∧F:X⟶0+∞→X∈V
25 23 24 fexd ⊢X∈V∧F:X⟶0+∞→F∈V
26 pnfxr ⊢+∞∈ℝ*
27 26 a1i ⊢X∈V∧F:X⟶0+∞→+∞∈ℝ*
28 xrltso ⊢<Orℝ*
29 28 supex ⊢supran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡wℝ*<∈V
30 29 a1i ⊢X∈V∧F:X⟶0+∞→supran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡wℝ*<∈V
31 27 30 ifexd ⊢X∈V∧F:X⟶0+∞→if+∞∈ran⁡F+∞supran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡wℝ*<∈V
32 2 22 25 31 fvmptd ⊢X∈V∧F:X⟶0+∞→sum^⁡F=if+∞∈ran⁡F+∞supran⁡y∈𝒫X∩Fin⟼∑w∈yF⁡wℝ*<