Metamath Proof Explorer

Theorem sge0sup

Description: The arbitrary sum of nonnegative extended reals is the supremum of finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0sup.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0sup.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
Assertion sge0sup ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 sge0sup.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0sup.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 eqidd ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ = +∞ )
4 1 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
5 2 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
6 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐹 )
7 4 5 6 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = +∞ )
8 vex ⊢ 𝑥 ∈ V
9 8 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ V )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
11 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑋 )
12 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
13 11 12 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ⊆ 𝑋 )
15 10 14 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
16 9 15 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
17 16 adantlr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
18 17 ralrimiva ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
19 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
20 19 rnmptss ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* )
21 18 20 syl ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* )
22 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
23 fvelrnb ⊢ ( 𝐹 Fn 𝑋 → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ ) )
24 22 23 syl ⊢ ( 𝜑 → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ ) )
26 6 25 mpbid ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ )
27 snelpwi ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ∈ 𝒫 𝑋 )
28 snfi ⊢ { 𝑦 } ∈ Fin
29 28 a1i ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ∈ Fin )
30 27 29 elind ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ∈ ( 𝒫 𝑋 ∩ Fin ) )
31 30 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → { 𝑦 } ∈ ( 𝒫 𝑋 ∩ Fin ) )
32 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → 𝑦 ∈ 𝑋 )
33 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
34 32 snssd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → { 𝑦 } ⊆ 𝑋 )
35 33 34 fssresd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( 𝐹 ↾ { 𝑦 } ) : { 𝑦 } ⟶ ( 0 [,] +∞ ) )
36 32 35 sge0sn ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( Σ^ ‘ ( 𝐹 ↾ { 𝑦 } ) ) = ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑦 ) )
37 vsnid ⊢ 𝑦 ∈ { 𝑦 }
38 fvres ⊢ ( 𝑦 ∈ { 𝑦 } → ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
39 37 38 ax-mp ⊢ ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 )
40 39 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( ( 𝐹 ↾ { 𝑦 } ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
41 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ( 𝐹 ‘ 𝑦 ) = +∞ )
42 36 40 41 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝐹 ↾ { 𝑦 } ) ) )
43 reseq2 ⊢ ( 𝑥 = { 𝑦 } → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ { 𝑦 } ) )
44 43 fveq2d ⊢ ( 𝑥 = { 𝑦 } → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝐹 ↾ { 𝑦 } ) ) )
45 44 rspceeqv ⊢ ( ( { 𝑦 } ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ +∞ = ( Σ^ ‘ ( 𝐹 ↾ { 𝑦 } ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) +∞ = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
46 31 42 45 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) +∞ = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
47 pnfex ⊢ +∞ ∈ V
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ ∈ V )
49 19 46 48 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = +∞ ) → +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
50 49 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 → ( ( 𝐹 ‘ 𝑦 ) = +∞ → +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) ) )
51 50 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ → +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = +∞ → +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) )
53 26 52 mpd ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
54 supxrpnf ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* ∧ +∞ ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ )
55 21 53 54 syl2anc ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = +∞ )
56 3 7 55 3eqtr4d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
57 1 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
58 2 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
59 simpr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ¬ +∞ ∈ ran 𝐹 )
60 58 59 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
61 57 60 sge0reval ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
62 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ Fin )
63 62 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
64 15 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
65 nelrnres ⊢ ( ¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝑥 ) )
66 65 ad2antlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝑥 ) )
67 64 66 fge0iccico ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,) +∞ ) )
68 63 67 sge0fsum ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) = Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) )
69 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
70 fvres ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
71 69 70 syl ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
72 71 sumeq2dv ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
74 68 73 eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
75 74 mpteq2dva ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
76 75 rneqd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) = ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
77 76 supeq1d ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
78 61 77 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
79 56 78 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )