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 +∞ sup ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w ℝ * <

Proof

Step Hyp Ref Expression
1 df-sumge0 ⊢ sum^ = x ∈ V ⟼ if +∞ ∈ ran ⁡ x +∞ sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * <
2 1 a1i ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ → sum^ = x ∈ V ⟼ if +∞ ∈ ran ⁡ x +∞ sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ 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 ∈ y x ⁡ w = y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y x ⁡ w
14 13 adantll ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ ∧ x = F → y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w = y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y x ⁡ w
15 fveq1 ⊢ x = F → x ⁡ w = F ⁡ w
16 15 sumeq2sdv ⊢ x = F → ∑ w ∈ y x ⁡ w = ∑ w ∈ y F ⁡ w
17 16 mpteq2dv ⊢ x = F → y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y x ⁡ w = y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w
18 17 adantl ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ ∧ x = F → y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y x ⁡ w = y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w
19 14 18 eqtrd ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ ∧ x = F → y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w = y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w
20 19 rneqd ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ ∧ x = F → ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w = ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w
21 20 supeq1d ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ ∧ x = F → sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * < = sup ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w ℝ * <
22 5 21 ifbieq2d ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ ∧ x = F → if +∞ ∈ ran ⁡ x +∞ sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * < = if +∞ ∈ ran ⁡ F +∞ sup ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ 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 ⊢ sup ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w ℝ * < ∈ V
30 29 a1i ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ → sup ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w ℝ * < ∈ V
31 27 30 ifexd ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ → if +∞ ∈ ran ⁡ F +∞ sup ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w ℝ * < ∈ V
32 2 22 25 31 fvmptd ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ → sum^ ⁡ F = if +∞ ∈ ran ⁡ F +∞ sup ran ⁡ y ∈ 𝒫 X ∩ Fin ⟼ ∑ w ∈ y F ⁡ w ℝ * <