Metamath Proof Explorer


Theorem esumadd

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

Ref Expression
Hypotheses esumadd.0
|- ( ph -> A e. V )
esumadd.1
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumadd.2
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
Assertion esumadd
|- ( 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 esumadd.0
 |-  ( ph -> A e. V )
2 esumadd.1
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
3 esumadd.2
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
4 nfv
 |-  F/ k ph
5 nfcv
 |-  F/_ k A
6 ge0xaddcl
 |-  ( ( B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B +e C ) e. ( 0 [,] +oo ) )
7 2 3 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 2 fmpttd
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
15 3 fmpttd
 |-  ( ph -> ( k e. A |-> C ) : A --> ( 0 [,] +oo ) )
16 4 5 1 2 esumel
 |-  ( ph -> sum* k e. A B e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
17 4 5 1 3 esumel
 |-  ( ph -> sum* k e. A C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) )
18 8 9 11 13 1 14 15 16 17 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 ) ) ) )
19 eqidd
 |-  ( ph -> ( k e. A |-> B ) = ( k e. A |-> B ) )
20 eqidd
 |-  ( ph -> ( k e. A |-> C ) = ( k e. A |-> C ) )
21 1 2 3 19 20 offval2
 |-  ( ph -> ( ( k e. A |-> B ) oF +e ( k e. A |-> C ) ) = ( k e. A |-> ( B +e C ) ) )
22 21 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 ) ) ) )
23 18 22 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 ) ) ) )
24 4 5 1 7 23 esumid
 |-  ( ph -> sum* k e. A ( B +e C ) = ( sum* k e. A B +e sum* k e. A C ) )