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 ⊢ Ⅎ _ k B
esumsnf.1 ⊢ φ ∧ k = M → A = B
esumsnf.2 ⊢ φ → M ∈ V
esumsnf.3 ⊢ φ → B ∈ 0 +∞
Assertion esumsnf ⊢ φ → ∑ * k ∈ M A = B

Proof

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