Metamath Proof Explorer

Theorem sumss

Description: Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014)

Ref Expression
Hypotheses sumss.1 
|- ( ph -> A C_ B )
sumss.2 
|- ( ( ph /\ k e. A ) -> C e. CC )
sumss.3 
|- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )
sumss.4 
|- ( ph -> B C_ ( ZZ>= ` M ) )
Assertion sumss 
|- ( ph -> sum_ k e. A C = sum_ k e. B C )

Proof

Step Hyp Ref Expression
1 sumss.1 
 |-  ( ph -> A C_ B )
2 sumss.2 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
3 sumss.3 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )
4 sumss.4 
 |-  ( ph -> B C_ ( ZZ>= ` M ) )
5 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
6 simpr 
 |-  ( ( ph /\ M e. ZZ ) -> M e. ZZ )
7 1 4 sstrd 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
8 7 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> A C_ ( ZZ>= ` M ) )
9 nfcv 
 |-  F/_ k m
10 nffvmpt1 
 |-  F/_ k ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m )
11 nfv 
 |-  F/ k m e. A
12 nffvmpt1 
 |-  F/_ k ( ( k e. A |-> C ) ` m )
13 nfcv 
 |-  F/_ k 0
14 11 12 13 nfif 
 |-  F/_ k if ( m e. A , ( ( k e. A |-> C ) ` m ) , 0 )
15 10 14 nfeq 
 |-  F/ k ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. A , ( ( k e. A |-> C ) ` m ) , 0 )
16 fveq2 
 |-  ( k = m -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) )
17 eleq1w 
 |-  ( k = m -> ( k e. A <-> m e. A ) )
18 fveq2 
 |-  ( k = m -> ( ( k e. A |-> C ) ` k ) = ( ( k e. A |-> C ) ` m ) )
19 17 18 ifbieq1d 
 |-  ( k = m -> if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) = if ( m e. A , ( ( k e. A |-> C ) ` m ) , 0 ) )
20 16 19 eqeq12d 
 |-  ( k = m -> ( ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) <-> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. A , ( ( k e. A |-> C ) ` m ) , 0 ) ) )
21 eqid 
 |-  ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) = ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) )
22 21 fvmpt2i 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = ( _I ` if ( k e. A , C , 0 ) ) )
23 iftrue 
 |-  ( k e. A -> if ( k e. A , C , 0 ) = C )
24 23 fveq2d 
 |-  ( k e. A -> ( _I ` if ( k e. A , C , 0 ) ) = ( _I ` C ) )
25 22 24 sylan9eq 
 |-  ( ( k e. ( ZZ>= ` M ) /\ k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = ( _I ` C ) )
26 iftrue 
 |-  ( k e. A -> if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) = ( ( k e. A |-> C ) ` k ) )
27 eqid 
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
28 27 fvmpt2i 
 |-  ( k e. A -> ( ( k e. A |-> C ) ` k ) = ( _I ` C ) )
29 26 28 eqtrd 
 |-  ( k e. A -> if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) = ( _I ` C ) )
30 29 adantl 
 |-  ( ( k e. ( ZZ>= ` M ) /\ k e. A ) -> if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) = ( _I ` C ) )
31 25 30 eqtr4d 
 |-  ( ( k e. ( ZZ>= ` M ) /\ k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) )
32 iffalse 
 |-  ( -. k e. A -> if ( k e. A , C , 0 ) = 0 )
33 32 fveq2d 
 |-  ( -. k e. A -> ( _I ` if ( k e. A , C , 0 ) ) = ( _I ` 0 ) )
34 0z 
 |-  0 e. ZZ
35 fvi 
 |-  ( 0 e. ZZ -> ( _I ` 0 ) = 0 )
36 34 35 ax-mp 
 |-  ( _I ` 0 ) = 0
37 33 36 eqtrdi 
 |-  ( -. k e. A -> ( _I ` if ( k e. A , C , 0 ) ) = 0 )
38 22 37 sylan9eq 
 |-  ( ( k e. ( ZZ>= ` M ) /\ -. k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = 0 )
39 iffalse 
 |-  ( -. k e. A -> if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) = 0 )
40 39 adantl 
 |-  ( ( k e. ( ZZ>= ` M ) /\ -. k e. A ) -> if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) = 0 )
41 38 40 eqtr4d 
 |-  ( ( k e. ( ZZ>= ` M ) /\ -. k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) )
42 31 41 pm2.61dan 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. A , ( ( k e. A |-> C ) ` k ) , 0 ) )
43 9 15 20 42 vtoclgaf 
 |-  ( m e. ( ZZ>= ` M ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. A , ( ( k e. A |-> C ) ` m ) , 0 ) )
44 43 adantl 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. A , ( ( k e. A |-> C ) ` m ) , 0 ) )
45 2 fmpttd 
 |-  ( ph -> ( k e. A |-> C ) : A --> CC )
46 45 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> ( k e. A |-> C ) : A --> CC )
47 46 ffvelcdmda 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> ( ( k e. A |-> C ) ` m ) e. CC )
48 5 6 8 44 47 zsum 
 |-  ( ( ph /\ M e. ZZ ) -> sum_ m e. A ( ( k e. A |-> C ) ` m ) = ( ~~> ` seq M ( + , ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ) ) )
49 4 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> B C_ ( ZZ>= ` M ) )
50 nfv 
 |-  F/ k ph
51 nfv 
 |-  F/ k m e. B
52 nffvmpt1 
 |-  F/_ k ( ( k e. B |-> C ) ` m )
53 51 52 13 nfif 
 |-  F/_ k if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 )
54 10 53 nfeq 
 |-  F/ k ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 )
55 50 54 nfim 
 |-  F/ k ( ph -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 ) )
56 eleq1w 
 |-  ( k = m -> ( k e. B <-> m e. B ) )
57 fveq2 
 |-  ( k = m -> ( ( k e. B |-> C ) ` k ) = ( ( k e. B |-> C ) ` m ) )
58 56 57 ifbieq1d 
 |-  ( k = m -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 ) )
59 16 58 eqeq12d 
 |-  ( k = m -> ( ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) <-> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 ) ) )
60 59 imbi2d 
 |-  ( k = m -> ( ( ph -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) ) <-> ( ph -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 ) ) ) )
61 25 adantll 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = ( _I ` C ) )
62 1 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> A C_ B )
63 62 sselda 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> k e. B )
64 iftrue 
 |-  ( k e. B -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = ( ( k e. B |-> C ) ` k ) )
65 eqid 
 |-  ( k e. B |-> C ) = ( k e. B |-> C )
66 65 fvmpt2i 
 |-  ( k e. B -> ( ( k e. B |-> C ) ` k ) = ( _I ` C ) )
67 64 66 eqtrd 
 |-  ( k e. B -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = ( _I ` C ) )
68 63 67 syl 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = ( _I ` C ) )
69 61 68 eqtr4d 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) )
70 38 adantll 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ -. k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = 0 )
71 67 ad2antrl 
 |-  ( ( ph /\ ( k e. B /\ -. k e. A ) ) -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = ( _I ` C ) )
72 eldif 
 |-  ( k e. ( B \ A ) <-> ( k e. B /\ -. k e. A ) )
73 3 fveq2d 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> ( _I ` C ) = ( _I ` 0 ) )
74 0cn 
 |-  0 e. CC
75 fvi 
 |-  ( 0 e. CC -> ( _I ` 0 ) = 0 )
76 74 75 ax-mp 
 |-  ( _I ` 0 ) = 0
77 73 76 eqtrdi 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> ( _I ` C ) = 0 )
78 72 77 sylan2br 
 |-  ( ( ph /\ ( k e. B /\ -. k e. A ) ) -> ( _I ` C ) = 0 )
79 71 78 eqtrd 
 |-  ( ( ph /\ ( k e. B /\ -. k e. A ) ) -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 )
80 79 expr 
 |-  ( ( ph /\ k e. B ) -> ( -. k e. A -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 ) )
81 iffalse 
 |-  ( -. k e. B -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 )
82 81 adantl 
 |-  ( ( ph /\ -. k e. B ) -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 )
83 82 a1d 
 |-  ( ( ph /\ -. k e. B ) -> ( -. k e. A -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 ) )
84 80 83 pm2.61dan 
 |-  ( ph -> ( -. k e. A -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 ) )
85 84 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( -. k e. A -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 ) )
86 85 imp 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ -. k e. A ) -> if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) = 0 )
87 70 86 eqtr4d 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ -. k e. A ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) )
88 69 87 pm2.61dan 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) )
89 88 expcom 
 |-  ( k e. ( ZZ>= ` M ) -> ( ph -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` k ) = if ( k e. B , ( ( k e. B |-> C ) ` k ) , 0 ) ) )
90 9 55 60 89 vtoclgaf 
 |-  ( m e. ( ZZ>= ` M ) -> ( ph -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 ) ) )
91 90 impcom 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 ) )
92 91 adantlr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 0 ) )
93 2 ex 
 |-  ( ph -> ( k e. A -> C e. CC ) )
94 93 adantr 
 |-  ( ( ph /\ k e. B ) -> ( k e. A -> C e. CC ) )
95 3 74 eqeltrdi 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. CC )
96 72 95 sylan2br 
 |-  ( ( ph /\ ( k e. B /\ -. k e. A ) ) -> C e. CC )
97 96 expr 
 |-  ( ( ph /\ k e. B ) -> ( -. k e. A -> C e. CC ) )
98 94 97 pm2.61d 
 |-  ( ( ph /\ k e. B ) -> C e. CC )
99 98 fmpttd 
 |-  ( ph -> ( k e. B |-> C ) : B --> CC )
100 99 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> ( k e. B |-> C ) : B --> CC )
101 100 ffvelcdmda 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> ( ( k e. B |-> C ) ` m ) e. CC )
102 5 6 49 92 101 zsum 
 |-  ( ( ph /\ M e. ZZ ) -> sum_ m e. B ( ( k e. B |-> C ) ` m ) = ( ~~> ` seq M ( + , ( k e. ( ZZ>= ` M ) |-> if ( k e. A , C , 0 ) ) ) ) )
103 48 102 eqtr4d 
 |-  ( ( ph /\ M e. ZZ ) -> sum_ m e. A ( ( k e. A |-> C ) ` m ) = sum_ m e. B ( ( k e. B |-> C ) ` m ) )
104 sumfc 
 |-  sum_ m e. A ( ( k e. A |-> C ) ` m ) = sum_ k e. A C
105 sumfc 
 |-  sum_ m e. B ( ( k e. B |-> C ) ` m ) = sum_ k e. B C
106 103 104 105 3eqtr3g 
 |-  ( ( ph /\ M e. ZZ ) -> sum_ k e. A C = sum_ k e. B C )
107 1 adantr 
 |-  ( ( ph /\ -. M e. ZZ ) -> A C_ B )
108 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
109 108 fdmi 
 |-  dom ZZ>= = ZZ
110 109 eleq2i 
 |-  ( M e. dom ZZ>= <-> M e. ZZ )
111 ndmfv 
 |-  ( -. M e. dom ZZ>= -> ( ZZ>= ` M ) = (/) )
112 110 111 sylnbir 
 |-  ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
113 112 sseq2d 
 |-  ( -. M e. ZZ -> ( B C_ ( ZZ>= ` M ) <-> B C_ (/) ) )
114 4 113 imbitrid 
 |-  ( -. M e. ZZ -> ( ph -> B C_ (/) ) )
115 114 impcom 
 |-  ( ( ph /\ -. M e. ZZ ) -> B C_ (/) )
116 107 115 sstrd 
 |-  ( ( ph /\ -. M e. ZZ ) -> A C_ (/) )
117 ss0 
 |-  ( A C_ (/) -> A = (/) )
118 116 117 syl 
 |-  ( ( ph /\ -. M e. ZZ ) -> A = (/) )
119 ss0 
 |-  ( B C_ (/) -> B = (/) )
120 115 119 syl 
 |-  ( ( ph /\ -. M e. ZZ ) -> B = (/) )
121 118 120 eqtr4d 
 |-  ( ( ph /\ -. M e. ZZ ) -> A = B )
122 121 sumeq1d 
 |-  ( ( ph /\ -. M e. ZZ ) -> sum_ k e. A C = sum_ k e. B C )
123 106 122 pm2.61dan 
 |-  ( ph -> sum_ k e. A C = sum_ k e. B C )