Metamath Proof Explorer

Theorem esumaddf

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

Ref Expression
Hypotheses esumaddf.0 
|- F/ k ph
esumaddf.a 
|- F/_ k A
esumaddf.1 
|- ( ph -> A e. V )
esumaddf.2 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumaddf.3 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
Assertion esumaddf 
|- ( ph -> sum* k e. A ( B +e C ) = ( sum* k e. A B +e sum* k e. A C ) )

Proof

Step Hyp Ref Expression
1 esumaddf.0 
 |-  F/ k ph
2 esumaddf.a 
 |-  F/_ k A
3 esumaddf.1 
 |-  ( ph -> A e. V )
4 esumaddf.2 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
5 esumaddf.3 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
6 ge0xaddcl 
 |-  ( ( B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B +e C ) e. ( 0 [,] +oo ) )
7 4 5 6 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( B +e C ) e. ( 0 [,] +oo ) )
8 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
9 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
10 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
11 10 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
12 xrge0tmd 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd
13 12 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd )
14 nfcv 
 |-  F/_ k ( 0 [,] +oo )
15 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
16 1 2 14 4 15 fmptdF 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
17 eqid 
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
18 1 2 14 5 17 fmptdF 
 |-  ( ph -> ( k e. A |-> C ) : A --> ( 0 [,] +oo ) )
19 1 2 3 4 esumel 
 |-  ( ph -> sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
20 1 2 3 5 esumel 
 |-  ( ph -> sum* k e. A C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) )
21 8 9 11 13 3 16 18 19 20 tsmsadd 
 |-  ( ph -> ( sum* k e. A B +e sum* k e. A C ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. A |-> B ) oF +e ( k e. A |-> C ) ) ) )
22 eqidd 
 |-  ( ph -> ( k e. A |-> B ) = ( k e. A |-> B ) )
23 eqidd 
 |-  ( ph -> ( k e. A |-> C ) = ( k e. A |-> C ) )
24 1 2 3 4 5 22 23 offval2f 
 |-  ( ph -> ( ( k e. A |-> B ) oF +e ( k e. A |-> C ) ) = ( k e. A |-> ( B +e C ) ) )
25 24 oveq2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. A |-> B ) oF +e ( k e. A |-> C ) ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> ( B +e C ) ) ) )
26 21 25 eleqtrd 
 |-  ( ph -> ( sum* k e. A B +e sum* k e. A C ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> ( B +e C ) ) ) )
27 1 2 3 7 26 esumid 
 |-  ( ph -> sum* k e. A ( B +e C ) = ( sum* k e. A B +e sum* k e. A C ) )