Metamath Proof Explorer


Theorem esumaddf

Description: Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017)

Ref Expression
Hypotheses esumaddf.0 kφ
esumaddf.a _kA
esumaddf.1 φAV
esumaddf.2 φkAB0+∞
esumaddf.3 φkAC0+∞
Assertion esumaddf φ*kAB+𝑒C=*kAB+𝑒*kAC

Proof

Step Hyp Ref Expression
1 esumaddf.0 kφ
2 esumaddf.a _kA
3 esumaddf.1 φAV
4 esumaddf.2 φkAB0+∞
5 esumaddf.3 φkAC0+∞
6 ge0xaddcl B0+∞C0+∞B+𝑒C0+∞
7 4 5 6 syl2anc φkAB+𝑒C0+∞
8 xrge0base 0+∞=Base𝑠*𝑠0+∞
9 xrge0plusg +𝑒=+𝑠*𝑠0+∞
10 xrge0cmn 𝑠*𝑠0+∞CMnd
11 10 a1i φ𝑠*𝑠0+∞CMnd
12 xrge0tmd 𝑠*𝑠0+∞TopMnd
13 12 a1i φ𝑠*𝑠0+∞TopMnd
14 nfcv _k0+∞
15 eqid kAB=kAB
16 1 2 14 4 15 fmptdF φkAB:A0+∞
17 eqid kAC=kAC
18 1 2 14 5 17 fmptdF φkAC:A0+∞
19 1 2 3 4 esumel φ*kAB𝑠*𝑠0+∞tsumskAB
20 1 2 3 5 esumel φ*kAC𝑠*𝑠0+∞tsumskAC
21 8 9 11 13 3 16 18 19 20 tsmsadd φ*kAB+𝑒*kAC𝑠*𝑠0+∞tsumskAB+𝑒fkAC
22 eqidd φkAB=kAB
23 eqidd φkAC=kAC
24 1 2 3 4 5 22 23 offval2f φkAB+𝑒fkAC=kAB+𝑒C
25 24 oveq2d φ𝑠*𝑠0+∞tsumskAB+𝑒fkAC=𝑠*𝑠0+∞tsumskAB+𝑒C
26 21 25 eleqtrd φ*kAB+𝑒*kAC𝑠*𝑠0+∞tsumskAB+𝑒C
27 1 2 3 7 26 esumid φ*kAB+𝑒C=*kAB+𝑒*kAC