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 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
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 ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = Σ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) )