Metamath Proof Explorer


Theorem esumss

Description: Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017)

Ref Expression
Hypotheses esumss.p kφ
esumss.a _kA
esumss.b _kB
esumss.1 φAB
esumss.2 φBV
esumss.3 φkBC0+∞
esumss.4 φkBAC=0
Assertion esumss φ*kAC=*kBC

Proof

Step Hyp Ref Expression
1 esumss.p kφ
2 esumss.a _kA
3 esumss.b _kB
4 esumss.1 φAB
5 esumss.2 φBV
6 esumss.3 φkBC0+∞
7 esumss.4 φkBAC=0
8 3 2 resmptf ABkBCA=kAC
9 4 8 syl φkBCA=kAC
10 9 oveq2d φ𝑠*𝑠0+∞tsumskBCA=𝑠*𝑠0+∞tsumskAC
11 xrge0base 0+∞=Base𝑠*𝑠0+∞
12 xrge00 0=0𝑠*𝑠0+∞
13 xrge0cmn 𝑠*𝑠0+∞CMnd
14 13 a1i φ𝑠*𝑠0+∞CMnd
15 xrge0tps 𝑠*𝑠0+∞TopSp
16 15 a1i φ𝑠*𝑠0+∞TopSp
17 nfcv _k0+∞
18 eqid kBC=kBC
19 1 3 17 6 18 fmptdF φkBC:B0+∞
20 1 3 2 7 5 suppss2f φkBCsupp0A
21 11 12 14 16 5 19 20 tsmsres φ𝑠*𝑠0+∞tsumskBCA=𝑠*𝑠0+∞tsumskBC
22 10 21 eqtr3d φ𝑠*𝑠0+∞tsumskAC=𝑠*𝑠0+∞tsumskBC
23 22 unieqd φ𝑠*𝑠0+∞tsumskAC=𝑠*𝑠0+∞tsumskBC
24 df-esum *kAC=𝑠*𝑠0+∞tsumskAC
25 df-esum *kBC=𝑠*𝑠0+∞tsumskBC
26 23 24 25 3eqtr4g φ*kAC=*kBC