Metamath Proof Explorer

Theorem esumpad

Description: Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020)

Ref Expression
Hypotheses esumpad.1 
|- ( ph -> A e. V )
esumpad.2 
|- ( ph -> B e. W )
esumpad.3 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
esumpad.4 
|- ( ( ph /\ k e. B ) -> C = 0 )
Assertion esumpad 
|- ( ph -> sum* k e. ( A u. B ) C = sum* k e. A C )

Proof

Step Hyp Ref Expression
1 esumpad.1 
 |-  ( ph -> A e. V )
2 esumpad.2 
 |-  ( ph -> B e. W )
3 esumpad.3 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
4 esumpad.4 
 |-  ( ( ph /\ k e. B ) -> C = 0 )
5 nfv 
 |-  F/ k ph
6 nfcv 
 |-  F/_ k A
7 nfcv 
 |-  F/_ k ( B \ A )
8 elex 
 |-  ( A e. V -> A e. _V )
9 1 8 syl 
 |-  ( ph -> A e. _V )
10 2 difexd 
 |-  ( ph -> ( B \ A ) e. _V )
11 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
12 11 a1i 
 |-  ( ph -> ( A i^i ( B \ A ) ) = (/) )
13 difssd 
 |-  ( ph -> ( B \ A ) C_ B )
14 13 sselda 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> k e. B )
15 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
16 4 15 eqeltrdi 
 |-  ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )
17 14 16 syldan 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. ( 0 [,] +oo ) )
18 5 6 7 9 10 12 3 17 esumsplit 
 |-  ( ph -> sum* k e. ( A u. ( B \ A ) ) C = ( sum* k e. A C +e sum* k e. ( B \ A ) C ) )
19 undif2 
 |-  ( A u. ( B \ A ) ) = ( A u. B )
20 esumeq1 
 |-  ( ( A u. ( B \ A ) ) = ( A u. B ) -> sum* k e. ( A u. ( B \ A ) ) C = sum* k e. ( A u. B ) C )
21 19 20 ax-mp 
 |-  sum* k e. ( A u. ( B \ A ) ) C = sum* k e. ( A u. B ) C
22 21 a1i 
 |-  ( ph -> sum* k e. ( A u. ( B \ A ) ) C = sum* k e. ( A u. B ) C )
23 14 4 syldan 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )
24 23 ralrimiva 
 |-  ( ph -> A. k e. ( B \ A ) C = 0 )
25 5 24 esumeq2d 
 |-  ( ph -> sum* k e. ( B \ A ) C = sum* k e. ( B \ A ) 0 )
26 7 esum0 
 |-  ( ( B \ A ) e. _V -> sum* k e. ( B \ A ) 0 = 0 )
27 10 26 syl 
 |-  ( ph -> sum* k e. ( B \ A ) 0 = 0 )
28 25 27 eqtrd 
 |-  ( ph -> sum* k e. ( B \ A ) C = 0 )
29 28 oveq2d 
 |-  ( ph -> ( sum* k e. A C +e sum* k e. ( B \ A ) C ) = ( sum* k e. A C +e 0 ) )
30 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
31 3 ralrimiva 
 |-  ( ph -> A. k e. A C e. ( 0 [,] +oo ) )
32 6 esumcl 
 |-  ( ( A e. V /\ A. k e. A C e. ( 0 [,] +oo ) ) -> sum* k e. A C e. ( 0 [,] +oo ) )
33 1 31 32 syl2anc 
 |-  ( ph -> sum* k e. A C e. ( 0 [,] +oo ) )
34 30 33 sselid 
 |-  ( ph -> sum* k e. A C e. RR* )
35 xaddid1 
 |-  ( sum* k e. A C e. RR* -> ( sum* k e. A C +e 0 ) = sum* k e. A C )
36 34 35 syl 
 |-  ( ph -> ( sum* k e. A C +e 0 ) = sum* k e. A C )
37 29 36 eqtrd 
 |-  ( ph -> ( sum* k e. A C +e sum* k e. ( B \ A ) C ) = sum* k e. A C )
38 18 22 37 3eqtr3d 
 |-  ( ph -> sum* k e. ( A u. B ) C = sum* k e. A C )