Metamath Proof Explorer

Theorem sge0sn

Description: A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0sn.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0sn.2 ⊢ ( 𝜑 → 𝐹 : { 𝐴 } ⟶ ( 0 [,] +∞ ) )
Assertion sge0sn ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sge0sn.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0sn.2 ⊢ ( 𝜑 → 𝐹 : { 𝐴 } ⟶ ( 0 [,] +∞ ) )
3 snex ⊢ { 𝐴 } ∈ V
4 3 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → { 𝐴 } ∈ V )
5 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → 𝐹 : { 𝐴 } ⟶ ( 0 [,] +∞ ) )
6 id ⊢ ( ( 𝐹 ‘ 𝐴 ) = +∞ → ( 𝐹 ‘ 𝐴 ) = +∞ )
7 6 eqcomd ⊢ ( ( 𝐹 ‘ 𝐴 ) = +∞ → +∞ = ( 𝐹 ‘ 𝐴 ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → +∞ = ( 𝐹 ‘ 𝐴 ) )
9 2 ffund ⊢ ( 𝜑 → Fun 𝐹 )
10 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → Fun 𝐹 )
11 snidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
12 1 11 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
13 2 fdmd ⊢ ( 𝜑 → dom 𝐹 = { 𝐴 } )
14 13 eqcomd ⊢ ( 𝜑 → { 𝐴 } = dom 𝐹 )
15 12 14 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ dom 𝐹 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → 𝐴 ∈ dom 𝐹 )
17 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
18 10 16 17 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
19 8 18 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → +∞ ∈ ran 𝐹 )
20 4 5 19 sge0pnfval ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) = +∞ )
21 simpr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( 𝐹 ‘ 𝐴 ) = +∞ )
22 20 21 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )
23 3 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → { 𝐴 } ∈ V )
24 2 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → 𝐹 : { 𝐴 } ⟶ ( 0 [,] +∞ ) )
25 elsni ⊢ ( +∞ ∈ { ( 𝐹 ‘ 𝐴 ) } → +∞ = ( 𝐹 ‘ 𝐴 ) )
26 25 eqcomd ⊢ ( +∞ ∈ { ( 𝐹 ‘ 𝐴 ) } → ( 𝐹 ‘ 𝐴 ) = +∞ )
27 26 con3i ⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = +∞ → ¬ +∞ ∈ { ( 𝐹 ‘ 𝐴 ) } )
28 27 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ¬ +∞ ∈ { ( 𝐹 ‘ 𝐴 ) } )
29 1 2 rnsnf ⊢ ( 𝜑 → ran 𝐹 = { ( 𝐹 ‘ 𝐴 ) } )
30 29 eqcomd ⊢ ( 𝜑 → { ( 𝐹 ‘ 𝐴 ) } = ran 𝐹 )
31 30 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → { ( 𝐹 ‘ 𝐴 ) } = ran 𝐹 )
32 28 31 neleqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ¬ +∞ ∈ ran 𝐹 )
33 24 32 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → 𝐹 : { 𝐴 } ⟶ ( 0 [,) +∞ ) )
34 23 33 sge0reval ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
35 sum0 ⊢ Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) = 0
36 35 eqcomi ⊢ 0 = Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 )
37 36 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → 0 = Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) )
38 nfcvd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → Ⅎ 𝑦 ( 𝐹 ‘ 𝐴 ) )
39 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ )
40 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
41 40 adantl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) ∧ 𝑦 = 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
42 1 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → 𝐴 ∈ 𝑉 )
43 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
44 ax-resscn ⊢ ℝ ⊆ ℂ
45 43 44 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
46 42 11 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → 𝐴 ∈ { 𝐴 } )
47 33 46 ffvelrnd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,) +∞ ) )
48 45 47 sseldi ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
49 38 39 41 42 48 sumsnd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
50 49 eqcomd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( 𝐹 ‘ 𝐴 ) = Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) )
51 37 50 preq12d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → { 0 , ( 𝐹 ‘ 𝐴 ) } = { Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) } )
52 51 supeq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → sup ( { 0 , ( 𝐹 ‘ 𝐴 ) } , ℝ* , < ) = sup ( { Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) } , ℝ* , < ) )
53 xrltso ⊢ < Or ℝ*
54 53 a1i ⊢ ( 𝜑 → < Or ℝ* )
55 0xr ⊢ 0 ∈ ℝ*
56 55 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
57 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
58 2 12 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
59 57 58 sseldi ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
60 suppr ⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → sup ( { 0 , ( 𝐹 ‘ 𝐴 ) } , ℝ* , < ) = if ( ( 𝐹 ‘ 𝐴 ) < 0 , 0 , ( 𝐹 ‘ 𝐴 ) ) )
61 54 56 59 60 syl3anc ⊢ ( 𝜑 → sup ( { 0 , ( 𝐹 ‘ 𝐴 ) } , ℝ* , < ) = if ( ( 𝐹 ‘ 𝐴 ) < 0 , 0 , ( 𝐹 ‘ 𝐴 ) ) )
62 pnfxr ⊢ +∞ ∈ ℝ*
63 62 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
64 56 63 58 3jca ⊢ ( 𝜑 → ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ) )
65 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
66 64 65 syl ⊢ ( 𝜑 → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
67 56 59 xrlenltd ⊢ ( 𝜑 → ( 0 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ¬ ( 𝐹 ‘ 𝐴 ) < 0 ) )
68 66 67 mpbid ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝐴 ) < 0 )
69 68 iffalsed ⊢ ( 𝜑 → if ( ( 𝐹 ‘ 𝐴 ) < 0 , 0 , ( 𝐹 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝐴 ) )
70 61 69 eqtr2d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = sup ( { 0 , ( 𝐹 ‘ 𝐴 ) } , ℝ* , < ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( 𝐹 ‘ 𝐴 ) = sup ( { 0 , ( 𝐹 ‘ 𝐴 ) } , ℝ* , < ) )
72 pwsn ⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }
73 72 ineq1i ⊢ ( 𝒫 { 𝐴 } ∩ Fin ) = ( { ∅ , { 𝐴 } } ∩ Fin )
74 0fin ⊢ ∅ ∈ Fin
75 snfi ⊢ { 𝐴 } ∈ Fin
76 prssi ⊢ ( ( ∅ ∈ Fin ∧ { 𝐴 } ∈ Fin ) → { ∅ , { 𝐴 } } ⊆ Fin )
77 74 75 76 mp2an ⊢ { ∅ , { 𝐴 } } ⊆ Fin
78 df-ss ⊢ ( { ∅ , { 𝐴 } } ⊆ Fin ↔ ( { ∅ , { 𝐴 } } ∩ Fin ) = { ∅ , { 𝐴 } } )
79 78 biimpi ⊢ ( { ∅ , { 𝐴 } } ⊆ Fin → ( { ∅ , { 𝐴 } } ∩ Fin ) = { ∅ , { 𝐴 } } )
80 77 79 ax-mp ⊢ ( { ∅ , { 𝐴 } } ∩ Fin ) = { ∅ , { 𝐴 } }
81 73 80 eqtri ⊢ ( 𝒫 { 𝐴 } ∩ Fin ) = { ∅ , { 𝐴 } }
82 mpteq1 ⊢ ( ( 𝒫 { 𝐴 } ∩ Fin ) = { ∅ , { 𝐴 } } → ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ { ∅ , { 𝐴 } } ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
83 81 82 ax-mp ⊢ ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ { ∅ , { 𝐴 } } ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
84 0ex ⊢ ∅ ∈ V
85 84 a1i ⊢ ( ⊤ → ∅ ∈ V )
86 3 a1i ⊢ ( ⊤ → { 𝐴 } ∈ V )
87 sumex ⊢ Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ∈ V
88 87 a1i ⊢ ( ⊤ → Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ∈ V )
89 sumex ⊢ Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ∈ V
90 89 a1i ⊢ ( ⊤ → Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ∈ V )
91 sumeq1 ⊢ ( 𝑥 = ∅ → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) )
92 91 adantl ⊢ ( ( ⊤ ∧ 𝑥 = ∅ ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) )
93 sumeq1 ⊢ ( 𝑥 = { 𝐴 } → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) )
94 93 adantl ⊢ ( ( ⊤ ∧ 𝑥 = { 𝐴 } ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) )
95 85 86 88 90 92 94 fmptpr ⊢ ( ⊤ → { ⟨ ∅ , Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ⟩ , ⟨ { 𝐴 } , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ⟩ } = ( 𝑥 ∈ { ∅ , { 𝐴 } } ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
96 95 mptru ⊢ { ⟨ ∅ , Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ⟩ , ⟨ { 𝐴 } , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ⟩ } = ( 𝑥 ∈ { ∅ , { 𝐴 } } ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
97 96 eqcomi ⊢ ( 𝑥 ∈ { ∅ , { 𝐴 } } ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = { ⟨ ∅ , Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ⟩ , ⟨ { 𝐴 } , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ⟩ }
98 83 97 eqtri ⊢ ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = { ⟨ ∅ , Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ⟩ , ⟨ { 𝐴 } , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ⟩ }
99 98 rneqi ⊢ ran ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ran { ⟨ ∅ , Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ⟩ , ⟨ { 𝐴 } , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ⟩ }
100 rnpropg ⊢ ( ( ∅ ∈ V ∧ { 𝐴 } ∈ V ) → ran { ⟨ ∅ , Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ⟩ , ⟨ { 𝐴 } , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ⟩ } = { Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) } )
101 84 3 100 mp2an ⊢ ran { ⟨ ∅ , Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ⟩ , ⟨ { 𝐴 } , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) ⟩ } = { Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) }
102 99 101 eqtri ⊢ ran ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = { Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) }
103 102 supeq1i ⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = sup ( { Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) } , ℝ* , < )
104 103 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → sup ( ran ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = sup ( { Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) , Σ 𝑦 ∈ { 𝐴 } ( 𝐹 ‘ 𝑦 ) } , ℝ* , < ) )
105 52 71 104 3eqtr4d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( 𝐹 ‘ 𝐴 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 { 𝐴 } ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
106 34 105 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )
107 22 106 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )