Metamath Proof Explorer

Theorem esumsnf

Description: The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017) (Revised by Thierry Arnoux, 2-May-2020)

Ref Expression
Hypotheses esumsnf.0 ⊢ Ⅎ 𝑘 𝐵
esumsnf.1 ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐵 )
esumsnf.2 ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
esumsnf.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion esumsnf ( 𝜑 → Σ* 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 esumsnf.0 ⊢ Ⅎ 𝑘 𝐵
2 esumsnf.1 ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐵 )
3 esumsnf.2 ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
4 esumsnf.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
5 df-esum ⊢ Σ* 𝑘 ∈ { 𝑀 } 𝐴 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) )
6 5 a1i ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑀 } 𝐴 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) )
7 eqid ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
8 snfi ⊢ { 𝑀 } ∈ Fin
9 8 a1i ⊢ ( 𝜑 → { 𝑀 } ∈ Fin )
10 elsni ⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
11 10 2 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝐴 = 𝐵 )
12 11 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐵 ) )
13 fmptsn ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → { ⟨ 𝑀 , 𝐵 ⟩ } = ( 𝑙 ∈ { 𝑀 } ↦ 𝐵 ) )
14 nfcv ⊢ Ⅎ 𝑙 𝐵
15 eqidd ⊢ ( 𝑘 = 𝑙 → 𝐵 = 𝐵 )
16 14 1 15 cbvmpt ⊢ ( 𝑘 ∈ { 𝑀 } ↦ 𝐵 ) = ( 𝑙 ∈ { 𝑀 } ↦ 𝐵 )
17 13 16 eqtr4di ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → { ⟨ 𝑀 , 𝐵 ⟩ } = ( 𝑘 ∈ { 𝑀 } ↦ 𝐵 ) )
18 3 4 17 syl2anc ⊢ ( 𝜑 → { ⟨ 𝑀 , 𝐵 ⟩ } = ( 𝑘 ∈ { 𝑀 } ↦ 𝐵 ) )
19 12 18 eqtr4d ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) = { ⟨ 𝑀 , 𝐵 ⟩ } )
20 fsng ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) : { 𝑀 } ⟶ { 𝐵 } ↔ ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) = { ⟨ 𝑀 , 𝐵 ⟩ } ) )
21 3 4 20 syl2anc ⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) : { 𝑀 } ⟶ { 𝐵 } ↔ ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) = { ⟨ 𝑀 , 𝐵 ⟩ } ) )
22 19 21 mpbird ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) : { 𝑀 } ⟶ { 𝐵 } )
23 4 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ ( 0 [,] +∞ ) )
24 22 23 fssd ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) : { 𝑀 } ⟶ ( 0 [,] +∞ ) )
25 xrltso ⊢ < Or ℝ*
26 25 a1i ⊢ ( 𝜑 → < Or ℝ* )
27 0xr ⊢ 0 ∈ ℝ*
28 27 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
29 elxrge0 ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) )
30 4 29 sylib ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) )
31 30 simpld ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
32 suppr ⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → sup ( { 0 , 𝐵 } , ℝ* , < ) = if ( 𝐵 < 0 , 0 , 𝐵 ) )
33 26 28 31 32 syl3anc ⊢ ( 𝜑 → sup ( { 0 , 𝐵 } , ℝ* , < ) = if ( 𝐵 < 0 , 0 , 𝐵 ) )
34 0fin ⊢ ∅ ∈ Fin
35 34 a1i ⊢ ( 𝜑 → ∅ ∈ Fin )
36 reseq2 ⊢ ( 𝑥 = ∅ → ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) = ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ ∅ ) )
37 res0 ⊢ ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ ∅ ) = ∅
38 36 37 eqtrdi ⊢ ( 𝑥 = ∅ → ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) = ∅ )
39 38 oveq2d ⊢ ( 𝑥 = ∅ → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ∅ ) )
40 xrge00 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
41 40 gsum0 ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ∅ ) = 0
42 39 41 eqtrdi ⊢ ( 𝑥 = ∅ → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) = 0 )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) = 0 )
44 reseq2 ⊢ ( 𝑥 = { 𝑀 } → ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) = ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ { 𝑀 } ) )
45 ssid ⊢ { 𝑀 } ⊆ { 𝑀 }
46 resmpt ⊢ ( { 𝑀 } ⊆ { 𝑀 } → ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) )
47 45 46 ax-mp ⊢ ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 )
48 44 47 eqtrdi ⊢ ( 𝑥 = { 𝑀 } → ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) )
49 48 oveq2d ⊢ ( 𝑥 = { 𝑀 } → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) )
50 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
51 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
52 cmnmnd ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
53 51 52 ax-mp ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
54 53 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
55 nfv ⊢ Ⅎ 𝑘 𝜑
56 50 54 3 4 2 55 1 gsumsnfd ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐵 )
57 49 56 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑥 = { 𝑀 } ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) = 𝐵 )
58 35 9 28 4 43 57 fmptpr ⊢ ( 𝜑 → { ⟨ ∅ , 0 ⟩ , ⟨ { 𝑀 } , 𝐵 ⟩ } = ( 𝑥 ∈ { ∅ , { 𝑀 } } ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) ) )
59 pwsn ⊢ 𝒫 { 𝑀 } = { ∅ , { 𝑀 } }
60 prssi ⊢ ( ( ∅ ∈ Fin ∧ { 𝑀 } ∈ Fin ) → { ∅ , { 𝑀 } } ⊆ Fin )
61 34 8 60 mp2an ⊢ { ∅ , { 𝑀 } } ⊆ Fin
62 59 61 eqsstri ⊢ 𝒫 { 𝑀 } ⊆ Fin
63 df-ss ⊢ ( 𝒫 { 𝑀 } ⊆ Fin ↔ ( 𝒫 { 𝑀 } ∩ Fin ) = 𝒫 { 𝑀 } )
64 62 63 mpbi ⊢ ( 𝒫 { 𝑀 } ∩ Fin ) = 𝒫 { 𝑀 }
65 64 59 eqtri ⊢ ( 𝒫 { 𝑀 } ∩ Fin ) = { ∅ , { 𝑀 } }
66 eqid ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) )
67 65 66 mpteq12i ⊢ ( 𝑥 ∈ ( 𝒫 { 𝑀 } ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) ) = ( 𝑥 ∈ { ∅ , { 𝑀 } } ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) )
68 58 67 eqtr4di ⊢ ( 𝜑 → { ⟨ ∅ , 0 ⟩ , ⟨ { 𝑀 } , 𝐵 ⟩ } = ( 𝑥 ∈ ( 𝒫 { 𝑀 } ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) ) )
69 68 rneqd ⊢ ( 𝜑 → ran { ⟨ ∅ , 0 ⟩ , ⟨ { 𝑀 } , 𝐵 ⟩ } = ran ( 𝑥 ∈ ( 𝒫 { 𝑀 } ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) ) )
70 rnpropg ⊢ ( ( ∅ ∈ Fin ∧ { 𝑀 } ∈ Fin ) → ran { ⟨ ∅ , 0 ⟩ , ⟨ { 𝑀 } , 𝐵 ⟩ } = { 0 , 𝐵 } )
71 35 9 70 syl2anc ⊢ ( 𝜑 → ran { ⟨ ∅ , 0 ⟩ , ⟨ { 𝑀 } , 𝐵 ⟩ } = { 0 , 𝐵 } )
72 69 71 eqtr3d ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 { 𝑀 } ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) ) = { 0 , 𝐵 } )
73 72 supeq1d ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 { 𝑀 } ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) ) , ℝ* , < ) = sup ( { 0 , 𝐵 } , ℝ* , < ) )
74 30 simprd ⊢ ( 𝜑 → 0 ≤ 𝐵 )
75 xrlenlt ⊢ ( ( 0 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 ↔ ¬ 𝐵 < 0 ) )
76 28 31 75 syl2anc ⊢ ( 𝜑 → ( 0 ≤ 𝐵 ↔ ¬ 𝐵 < 0 ) )
77 74 76 mpbid ⊢ ( 𝜑 → ¬ 𝐵 < 0 )
78 eqidd ⊢ ( 𝜑 → 𝐵 = 𝐵 )
79 77 78 jca ⊢ ( 𝜑 → ( ¬ 𝐵 < 0 ∧ 𝐵 = 𝐵 ) )
80 79 olcd ⊢ ( 𝜑 → ( ( 𝐵 < 0 ∧ 𝐵 = 0 ) ∨ ( ¬ 𝐵 < 0 ∧ 𝐵 = 𝐵 ) ) )
81 eqif ⊢ ( 𝐵 = if ( 𝐵 < 0 , 0 , 𝐵 ) ↔ ( ( 𝐵 < 0 ∧ 𝐵 = 0 ) ∨ ( ¬ 𝐵 < 0 ∧ 𝐵 = 𝐵 ) ) )
82 80 81 sylibr ⊢ ( 𝜑 → 𝐵 = if ( 𝐵 < 0 , 0 , 𝐵 ) )
83 33 73 82 3eqtr4rd ⊢ ( 𝜑 → 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 { 𝑀 } ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ↾ 𝑥 ) ) ) , ℝ* , < ) )
84 7 9 24 83 xrge0tsmsd ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = { 𝐵 } )
85 84 unieqd ⊢ ( 𝜑 → ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = ∪ { 𝐵 } )
86 unisng ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → ∪ { 𝐵 } = 𝐵 )
87 4 86 syl ⊢ ( 𝜑 → ∪ { 𝐵 } = 𝐵 )
88 6 85 87 3eqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )