Metamath Proof Explorer


Theorem sge0fsum

Description: The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0fsum.x ( 𝜑𝑋 ∈ Fin )
sge0fsum.f ( 𝜑𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
Assertion sge0fsum ( 𝜑 → ( Σ^𝐹 ) = Σ 𝑥𝑋 ( 𝐹𝑥 ) )

Proof

Step Hyp Ref Expression
1 sge0fsum.x ( 𝜑𝑋 ∈ Fin )
2 sge0fsum.f ( 𝜑𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
3 2 fge0icoicc ( 𝜑𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
4 1 3 sge0xrcl ( 𝜑 → ( Σ^𝐹 ) ∈ ℝ* )
5 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
6 2 ffvelrnda ( ( 𝜑𝑥𝑋 ) → ( 𝐹𝑥 ) ∈ ( 0 [,) +∞ ) )
7 5 6 sseldi ( ( 𝜑𝑥𝑋 ) → ( 𝐹𝑥 ) ∈ ℝ )
8 1 7 fsumrecl ( 𝜑 → Σ 𝑥𝑋 ( 𝐹𝑥 ) ∈ ℝ )
9 8 rexrd ( 𝜑 → Σ 𝑥𝑋 ( 𝐹𝑥 ) ∈ ℝ* )
10 1 2 sge0reval ( 𝜑 → ( Σ^𝐹 ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) , ℝ* , < ) )
11 simpr ( ( 𝜑𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ) → 𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) )
12 vex 𝑤 ∈ V
13 12 a1i ( ( 𝜑𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ) → 𝑤 ∈ V )
14 eqid ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) = ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) )
15 14 elrnmpt ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) ) )
16 13 15 syl ( ( 𝜑𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ) → ( 𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) ) )
17 11 16 mpbid ( ( 𝜑𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) )
18 simp3 ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) ) → 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) )
19 1 adantr ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑋 ∈ Fin )
20 2 fge0npnf ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
21 3 20 fge0iccre ( 𝜑𝐹 : 𝑋 ⟶ ℝ )
22 21 adantr ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ℝ )
23 22 adantr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑋 ) → 𝐹 : 𝑋 ⟶ ℝ )
24 simpr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑋 ) → 𝑥𝑋 )
25 23 24 ffvelrnd ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑋 ) → ( 𝐹𝑥 ) ∈ ℝ )
26 0xr 0 ∈ ℝ*
27 26 a1i ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑋 ) → 0 ∈ ℝ* )
28 pnfxr +∞ ∈ ℝ*
29 28 a1i ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑋 ) → +∞ ∈ ℝ* )
30 3 adantr ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
31 30 ffvelrnda ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑋 ) → ( 𝐹𝑥 ) ∈ ( 0 [,] +∞ ) )
32 iccgelb ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹𝑥 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝐹𝑥 ) )
33 27 29 31 32 syl3anc ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑋 ) → 0 ≤ ( 𝐹𝑥 ) )
34 elinel1 ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑦 ∈ 𝒫 𝑋 )
35 elpwi ( 𝑦 ∈ 𝒫 𝑋𝑦𝑋 )
36 34 35 syl ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑦𝑋 )
37 36 adantl ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑦𝑋 )
38 19 25 33 37 fsumless ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑥𝑦 ( 𝐹𝑥 ) ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) )
39 38 3adant3 ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) ) → Σ 𝑥𝑦 ( 𝐹𝑥 ) ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) )
40 18 39 eqbrtrd ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) ) → 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) )
41 40 3exp ( 𝜑 → ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) → 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) ) ) )
42 41 rexlimdv ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) → 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) ) )
43 42 adantr ( ( 𝜑𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ) → ( ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑥𝑦 ( 𝐹𝑥 ) → 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) ) )
44 17 43 mpd ( ( 𝜑𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ) → 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) )
45 44 ralrimiva ( 𝜑 → ∀ 𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) )
46 elinel2 ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑦 ∈ Fin )
47 46 adantl ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑦 ∈ Fin )
48 22 adantr ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑦 ) → 𝐹 : 𝑋 ⟶ ℝ )
49 37 sselda ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑦 ) → 𝑥𝑋 )
50 48 49 ffvelrnd ( ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥𝑦 ) → ( 𝐹𝑥 ) ∈ ℝ )
51 47 50 fsumrecl ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑥𝑦 ( 𝐹𝑥 ) ∈ ℝ )
52 51 rexrd ( ( 𝜑𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑥𝑦 ( 𝐹𝑥 ) ∈ ℝ* )
53 52 ralrimiva ( 𝜑 → ∀ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑥𝑦 ( 𝐹𝑥 ) ∈ ℝ* )
54 14 rnmptss ( ∀ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑥𝑦 ( 𝐹𝑥 ) ∈ ℝ* → ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ⊆ ℝ* )
55 53 54 syl ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ⊆ ℝ* )
56 supxrleub ( ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) ⊆ ℝ* ∧ Σ 𝑥𝑋 ( 𝐹𝑥 ) ∈ ℝ* ) → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) , ℝ* , < ) ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) ) )
57 55 9 56 syl2anc ( 𝜑 → ( sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) , ℝ* , < ) ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) 𝑤 ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) ) )
58 45 57 mpbird ( 𝜑 → sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑥𝑦 ( 𝐹𝑥 ) ) , ℝ* , < ) ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) )
59 10 58 eqbrtrd ( 𝜑 → ( Σ^𝐹 ) ≤ Σ 𝑥𝑋 ( 𝐹𝑥 ) )
60 ssid 𝑋𝑋
61 60 a1i ( 𝜑𝑋𝑋 )
62 1 2 61 1 fsumlesge0 ( 𝜑 → Σ 𝑥𝑋 ( 𝐹𝑥 ) ≤ ( Σ^𝐹 ) )
63 4 9 59 62 xrletrid ( 𝜑 → ( Σ^𝐹 ) = Σ 𝑥𝑋 ( 𝐹𝑥 ) )