Metamath Proof Explorer

Theorem sumss2

Description: Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013) (Revised by Mario Carneiro, 20-Apr-2014)

Ref Expression
Assertion sumss2 
|- ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ ( B C_ ( ZZ>= ` M ) \/ B e. Fin ) ) -> sum_ k e. A C = sum_ k e. B if ( k e. A , C , 0 ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B C_ ( ZZ>= ` M ) ) -> A C_ B )
2 iftrue 
 |-  ( m e. A -> if ( m e. A , [_ m / k ]_ C , 0 ) = [_ m / k ]_ C )
3 2 adantl 
 |-  ( ( A. k e. A C e. CC /\ m e. A ) -> if ( m e. A , [_ m / k ]_ C , 0 ) = [_ m / k ]_ C )
4 nfcsb1v 
 |-  F/_ k [_ m / k ]_ C
5 4 nfel1 
 |-  F/ k [_ m / k ]_ C e. CC
6 csbeq1a 
 |-  ( k = m -> C = [_ m / k ]_ C )
7 6 eleq1d 
 |-  ( k = m -> ( C e. CC <-> [_ m / k ]_ C e. CC ) )
8 5 7 rspc 
 |-  ( m e. A -> ( A. k e. A C e. CC -> [_ m / k ]_ C e. CC ) )
9 8 impcom 
 |-  ( ( A. k e. A C e. CC /\ m e. A ) -> [_ m / k ]_ C e. CC )
10 3 9 eqeltrd 
 |-  ( ( A. k e. A C e. CC /\ m e. A ) -> if ( m e. A , [_ m / k ]_ C , 0 ) e. CC )
11 10 ad4ant24 
 |-  ( ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B C_ ( ZZ>= ` M ) ) /\ m e. A ) -> if ( m e. A , [_ m / k ]_ C , 0 ) e. CC )
12 eldifn 
 |-  ( m e. ( B \ A ) -> -. m e. A )
13 12 iffalsed 
 |-  ( m e. ( B \ A ) -> if ( m e. A , [_ m / k ]_ C , 0 ) = 0 )
14 13 adantl 
 |-  ( ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B C_ ( ZZ>= ` M ) ) /\ m e. ( B \ A ) ) -> if ( m e. A , [_ m / k ]_ C , 0 ) = 0 )
15 simpr 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B C_ ( ZZ>= ` M ) ) -> B C_ ( ZZ>= ` M ) )
16 1 11 14 15 sumss 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B C_ ( ZZ>= ` M ) ) -> sum_ m e. A if ( m e. A , [_ m / k ]_ C , 0 ) = sum_ m e. B if ( m e. A , [_ m / k ]_ C , 0 ) )
17 simpll 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B e. Fin ) -> A C_ B )
18 10 ad4ant24 
 |-  ( ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B e. Fin ) /\ m e. A ) -> if ( m e. A , [_ m / k ]_ C , 0 ) e. CC )
19 13 adantl 
 |-  ( ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B e. Fin ) /\ m e. ( B \ A ) ) -> if ( m e. A , [_ m / k ]_ C , 0 ) = 0 )
20 simpr 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B e. Fin ) -> B e. Fin )
21 17 18 19 20 fsumss 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ B e. Fin ) -> sum_ m e. A if ( m e. A , [_ m / k ]_ C , 0 ) = sum_ m e. B if ( m e. A , [_ m / k ]_ C , 0 ) )
22 16 21 jaodan 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ ( B C_ ( ZZ>= ` M ) \/ B e. Fin ) ) -> sum_ m e. A if ( m e. A , [_ m / k ]_ C , 0 ) = sum_ m e. B if ( m e. A , [_ m / k ]_ C , 0 ) )
23 iftrue 
 |-  ( k e. A -> if ( k e. A , C , 0 ) = C )
24 23 sumeq2i 
 |-  sum_ k e. A if ( k e. A , C , 0 ) = sum_ k e. A C
25 nfcv 
 |-  F/_ m if ( k e. A , C , 0 )
26 nfv 
 |-  F/ k m e. A
27 nfcv 
 |-  F/_ k 0
28 26 4 27 nfif 
 |-  F/_ k if ( m e. A , [_ m / k ]_ C , 0 )
29 eleq1w 
 |-  ( k = m -> ( k e. A <-> m e. A ) )
30 29 6 ifbieq1d 
 |-  ( k = m -> if ( k e. A , C , 0 ) = if ( m e. A , [_ m / k ]_ C , 0 ) )
31 25 28 30 cbvsumi 
 |-  sum_ k e. A if ( k e. A , C , 0 ) = sum_ m e. A if ( m e. A , [_ m / k ]_ C , 0 )
32 24 31 eqtr3i 
 |-  sum_ k e. A C = sum_ m e. A if ( m e. A , [_ m / k ]_ C , 0 )
33 25 28 30 cbvsumi 
 |-  sum_ k e. B if ( k e. A , C , 0 ) = sum_ m e. B if ( m e. A , [_ m / k ]_ C , 0 )
34 22 32 33 3eqtr4g 
 |-  ( ( ( A C_ B /\ A. k e. A C e. CC ) /\ ( B C_ ( ZZ>= ` M ) \/ B e. Fin ) ) -> sum_ k e. A C = sum_ k e. B if ( k e. A , C , 0 ) )