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 _kB
esumsnf.1 φk=MA=B
esumsnf.2 φMV
esumsnf.3 φB0+∞
Assertion esumsnf φ*kMA=B

Proof

Step Hyp Ref Expression
1 esumsnf.0 _kB
2 esumsnf.1 φk=MA=B
3 esumsnf.2 φMV
4 esumsnf.3 φB0+∞
5 df-esum *kMA=𝑠*𝑠0+∞tsumskMA
6 5 a1i φ*kMA=𝑠*𝑠0+∞tsumskMA
7 eqid 𝑠*𝑠0+∞=𝑠*𝑠0+∞
8 snfi MFin
9 8 a1i φMFin
10 elsni kMk=M
11 10 2 sylan2 φkMA=B
12 11 mpteq2dva φkMA=kMB
13 fmptsn MVB0+∞MB=lMB
14 nfcv _lB
15 eqidd k=lB=B
16 14 1 15 cbvmpt kMB=lMB
17 13 16 eqtr4di MVB0+∞MB=kMB
18 3 4 17 syl2anc φMB=kMB
19 12 18 eqtr4d φkMA=MB
20 fsng MVB0+∞kMA:MBkMA=MB
21 3 4 20 syl2anc φkMA:MBkMA=MB
22 19 21 mpbird φkMA:MB
23 4 snssd φB0+∞
24 22 23 fssd φkMA:M0+∞
25 xrltso <Or*
26 25 a1i φ<Or*
27 0xr 0*
28 27 a1i φ0*
29 elxrge0 B0+∞B*0B
30 4 29 sylib φB*0B
31 30 simpld φB*
32 suppr <Or*0*B*sup0B*<=ifB<00B
33 26 28 31 32 syl3anc φsup0B*<=ifB<00B
34 0fin Fin
35 34 a1i φFin
36 reseq2 x=kMAx=kMA
37 res0 kMA=
38 36 37 eqtrdi x=kMAx=
39 38 oveq2d x=𝑠*𝑠0+∞kMAx=𝑠*𝑠0+∞
40 xrge00 0=0𝑠*𝑠0+∞
41 40 gsum0 𝑠*𝑠0+∞=0
42 39 41 eqtrdi x=𝑠*𝑠0+∞kMAx=0
43 42 adantl φx=𝑠*𝑠0+∞kMAx=0
44 reseq2 x=MkMAx=kMAM
45 ssid MM
46 resmpt MMkMAM=kMA
47 45 46 ax-mp kMAM=kMA
48 44 47 eqtrdi x=MkMAx=kMA
49 48 oveq2d x=M𝑠*𝑠0+∞kMAx=𝑠*𝑠0+∞kMA
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+∞kMA=B
57 49 56 sylan9eqr φx=M𝑠*𝑠0+∞kMAx=B
58 35 9 28 4 43 57 fmptpr φ0MB=xM𝑠*𝑠0+∞kMAx
59 pwsn 𝒫M=M
60 prssi FinMFinMFin
61 34 8 60 mp2an MFin
62 59 61 eqsstri 𝒫MFin
63 df-ss 𝒫MFin𝒫MFin=𝒫M
64 62 63 mpbi 𝒫MFin=𝒫M
65 64 59 eqtri 𝒫MFin=M
66 eqid 𝑠*𝑠0+∞kMAx=𝑠*𝑠0+∞kMAx
67 65 66 mpteq12i x𝒫MFin𝑠*𝑠0+∞kMAx=xM𝑠*𝑠0+∞kMAx
68 58 67 eqtr4di φ0MB=x𝒫MFin𝑠*𝑠0+∞kMAx
69 68 rneqd φran0MB=ranx𝒫MFin𝑠*𝑠0+∞kMAx
70 rnpropg FinMFinran0MB=0B
71 35 9 70 syl2anc φran0MB=0B
72 69 71 eqtr3d φranx𝒫MFin𝑠*𝑠0+∞kMAx=0B
73 72 supeq1d φsupranx𝒫MFin𝑠*𝑠0+∞kMAx*<=sup0B*<
74 30 simprd φ0B
75 xrlenlt 0*B*0B¬B<0
76 28 31 75 syl2anc φ0B¬B<0
77 74 76 mpbid φ¬B<0
78 eqidd φB=B
79 77 78 jca φ¬B<0B=B
80 79 olcd φB<0B=0¬B<0B=B
81 eqif B=ifB<00BB<0B=0¬B<0B=B
82 80 81 sylibr φB=ifB<00B
83 33 73 82 3eqtr4rd φB=supranx𝒫MFin𝑠*𝑠0+∞kMAx*<
84 7 9 24 83 xrge0tsmsd φ𝑠*𝑠0+∞tsumskMA=B
85 84 unieqd φ𝑠*𝑠0+∞tsumskMA=B
86 unisng B0+∞B=B
87 4 86 syl φB=B
88 6 85 87 3eqtrd φ*kMA=B