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 
|- F/ k ph
esumss.a 
|- F/_ k A
esumss.b 
|- F/_ k B
esumss.1 
|- ( ph -> A C_ B )
esumss.2 
|- ( ph -> B e. V )
esumss.3 
|- ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )
esumss.4 
|- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )
Assertion esumss 
|- ( ph -> sum* k e. A C = sum* k e. B C )

Proof

Step Hyp Ref Expression
1 esumss.p 
 |-  F/ k ph
2 esumss.a 
 |-  F/_ k A
3 esumss.b 
 |-  F/_ k B
4 esumss.1 
 |-  ( ph -> A C_ B )
5 esumss.2 
 |-  ( ph -> B e. V )
6 esumss.3 
 |-  ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )
7 esumss.4 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )
8 3 2 resmptf 
 |-  ( A C_ B -> ( ( k e. B |-> C ) |` A ) = ( k e. A |-> C ) )
9 4 8 syl 
 |-  ( ph -> ( ( k e. B |-> C ) |` A ) = ( k e. A |-> C ) )
10 9 oveq2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. B |-> C ) |` A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) )
11 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
12 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
13 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
14 13 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
15 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
16 15 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
17 nfcv 
 |-  F/_ k ( 0 [,] +oo )
18 eqid 
 |-  ( k e. B |-> C ) = ( k e. B |-> C )
19 1 3 17 6 18 fmptdF 
 |-  ( ph -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) )
20 1 3 2 7 5 suppss2f 
 |-  ( ph -> ( ( k e. B |-> C ) supp 0 ) C_ A )
21 11 12 14 16 5 19 20 tsmsres 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. B |-> C ) |` A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> C ) ) )
22 10 21 eqtr3d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> C ) ) )
23 22 unieqd 
 |-  ( ph -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) ) = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> C ) ) )
24 df-esum 
 |-  sum* k e. A C = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
25 df-esum 
 |-  sum* k e. B C = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. B |-> C ) )
26 23 24 25 3eqtr4g 
 |-  ( ph -> sum* k e. A C = sum* k e. B C )