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 ffvelrnda
 |-  ( ( ( 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 ffvelrnda
 |-  ( ( ( 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 syl5ib
 |-  ( -. 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 )