Metamath Proof Explorer

Theorem esumsplit

Description: Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017)

Ref Expression
Hypotheses esumsplit.1 
|- F/ k ph
esumsplit.2 
|- F/_ k A
esumsplit.3 
|- F/_ k B
esumsplit.4 
|- ( ph -> A e. _V )
esumsplit.5 
|- ( ph -> B e. _V )
esumsplit.6 
|- ( ph -> ( A i^i B ) = (/) )
esumsplit.7 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
esumsplit.8 
|- ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )
Assertion esumsplit 
|- ( ph -> sum* k e. ( A u. B ) C = ( sum* k e. A C +e sum* k e. B C ) )

Proof

Step Hyp Ref Expression
1 esumsplit.1 
 |-  F/ k ph
2 esumsplit.2 
 |-  F/_ k A
3 esumsplit.3 
 |-  F/_ k B
4 esumsplit.4 
 |-  ( ph -> A e. _V )
5 esumsplit.5 
 |-  ( ph -> B e. _V )
6 esumsplit.6 
 |-  ( ph -> ( A i^i B ) = (/) )
7 esumsplit.7 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
8 esumsplit.8 
 |-  ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )
9 2 3 nfun 
 |-  F/_ k ( A u. B )
10 unexg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
11 4 5 10 syl2anc 
 |-  ( ph -> ( A u. B ) e. _V )
12 elun 
 |-  ( k e. ( A u. B ) <-> ( k e. A \/ k e. B ) )
13 7 8 jaodan 
 |-  ( ( ph /\ ( k e. A \/ k e. B ) ) -> C e. ( 0 [,] +oo ) )
14 12 13 sylan2b 
 |-  ( ( ph /\ k e. ( A u. B ) ) -> C e. ( 0 [,] +oo ) )
15 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
16 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
17 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
18 17 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
19 xrge0tmd 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd
20 19 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd )
21 nfcv 
 |-  F/_ k ( 0 [,] +oo )
22 eqid 
 |-  ( k e. ( A u. B ) |-> C ) = ( k e. ( A u. B ) |-> C )
23 1 9 21 14 22 fmptdF 
 |-  ( ph -> ( k e. ( A u. B ) |-> C ) : ( A u. B ) --> ( 0 [,] +oo ) )
24 1 2 4 7 esumel 
 |-  ( ph -> sum* k e. A C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) )
25 ssun1 
 |-  A C_ ( A u. B )
26 9 2 resmptf 
 |-  ( A C_ ( A u. B ) -> ( ( k e. ( A u. B ) |-> C ) |` A ) = ( k e. A |-> C ) )
27 25 26 mp1i 
 |-  ( ph -> ( ( k e. ( A u. B ) |-> C ) |` A ) = ( k e. A |-> C ) )
28 27 oveq2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. ( A u. B ) |-> C ) |` A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) )
29 24 28 eleqtrrd 
 |-  ( ph -> sum* k e. A C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. ( A u. B ) |-> C ) |` A ) ) )
30 1 3 5 8 esumel 
 |-  ( ph -> sum* k e. B C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> C ) ) )
31 ssun2 
 |-  B C_ ( A u. B )
32 9 3 resmptf 
 |-  ( B C_ ( A u. B ) -> ( ( k e. ( A u. B ) |-> C ) |` B ) = ( k e. B |-> C ) )
33 31 32 mp1i 
 |-  ( ph -> ( ( k e. ( A u. B ) |-> C ) |` B ) = ( k e. B |-> C ) )
34 33 oveq2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. ( A u. B ) |-> C ) |` B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> C ) ) )
35 30 34 eleqtrrd 
 |-  ( ph -> sum* k e. B C e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. ( A u. B ) |-> C ) |` B ) ) )
36 eqidd 
 |-  ( ph -> ( A u. B ) = ( A u. B ) )
37 15 16 18 20 11 23 29 35 6 36 tsmssplit 
 |-  ( ph -> ( sum* k e. A C +e sum* k e. B C ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. ( A u. B ) |-> C ) ) )
38 1 9 11 14 37 esumid 
 |-  ( ph -> sum* k e. ( A u. B ) C = ( sum* k e. A C +e sum* k e. B C ) )