Metamath Proof Explorer

Theorem fsumss

Description: Change the index set to a subset in a finite 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 )
fsumss.4 
|- ( ph -> B e. Fin )
Assertion fsumss 
|- ( 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 fsumss.4 
 |-  ( ph -> B e. Fin )
5 1 adantr 
 |-  ( ( ph /\ B = (/) ) -> A C_ B )
6 2 adantlr 
 |-  ( ( ( ph /\ B = (/) ) /\ k e. A ) -> C e. CC )
7 3 adantlr 
 |-  ( ( ( ph /\ B = (/) ) /\ k e. ( B \ A ) ) -> C = 0 )
8 simpr 
 |-  ( ( ph /\ B = (/) ) -> B = (/) )
9 0ss 
 |-  (/) C_ ( ZZ>= ` 0 )
10 8 9 eqsstrdi 
 |-  ( ( ph /\ B = (/) ) -> B C_ ( ZZ>= ` 0 ) )
11 5 6 7 10 sumss 
 |-  ( ( ph /\ B = (/) ) -> sum_ k e. A C = sum_ k e. B C )
12 11 ex 
 |-  ( ph -> ( B = (/) -> sum_ k e. A C = sum_ k e. B C ) )
13 cnvimass 
 |-  ( `' f " A ) C_ dom f
14 simprr 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) -1-1-onto-> B )
15 f1of 
 |-  ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> f : ( 1 ... ( # ` B ) ) --> B )
16 14 15 syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) --> B )
17 13 16 fssdm 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( `' f " A ) C_ ( 1 ... ( # ` B ) ) )
18 16 ffnd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f Fn ( 1 ... ( # ` B ) ) )
19 elpreima 
 |-  ( f Fn ( 1 ... ( # ` B ) ) -> ( n e. ( `' f " A ) <-> ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) ) )
20 18 19 syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( n e. ( `' f " A ) <-> ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) ) )
21 16 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( 1 ... ( # ` B ) ) ) -> ( f ` n ) e. B )
22 21 ex 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( n e. ( 1 ... ( # ` B ) ) -> ( f ` n ) e. B ) )
23 22 adantrd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) -> ( f ` n ) e. B ) )
24 20 23 sylbid 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( n e. ( `' f " A ) -> ( f ` n ) e. B ) )
25 24 imp 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( `' f " A ) ) -> ( f ` n ) e. B )
26 2 ex 
 |-  ( ph -> ( k e. A -> C e. CC ) )
27 26 adantr 
 |-  ( ( ph /\ k e. B ) -> ( k e. A -> C e. CC ) )
28 eldif 
 |-  ( k e. ( B \ A ) <-> ( k e. B /\ -. k e. A ) )
29 0cn 
 |-  0 e. CC
30 3 29 eqeltrdi 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. CC )
31 28 30 sylan2br 
 |-  ( ( ph /\ ( k e. B /\ -. k e. A ) ) -> C e. CC )
32 31 expr 
 |-  ( ( ph /\ k e. B ) -> ( -. k e. A -> C e. CC ) )
33 27 32 pm2.61d 
 |-  ( ( ph /\ k e. B ) -> C e. CC )
34 33 fmpttd 
 |-  ( ph -> ( k e. B |-> C ) : B --> CC )
35 34 adantr 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( k e. B |-> C ) : B --> CC )
36 35 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ ( f ` n ) e. B ) -> ( ( k e. B |-> C ) ` ( f ` n ) ) e. CC )
37 25 36 syldan 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( `' f " A ) ) -> ( ( k e. B |-> C ) ` ( f ` n ) ) e. CC )
38 eldifi 
 |-  ( n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) -> n e. ( 1 ... ( # ` B ) ) )
39 38 21 sylan2 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( f ` n ) e. B )
40 eldifn 
 |-  ( n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) -> -. n e. ( `' f " A ) )
41 40 adantl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> -. n e. ( `' f " A ) )
42 38 adantl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> n e. ( 1 ... ( # ` B ) ) )
43 20 adantr 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( n e. ( `' f " A ) <-> ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) ) )
44 42 43 mpbirand 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( n e. ( `' f " A ) <-> ( f ` n ) e. A ) )
45 41 44 mtbid 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> -. ( f ` n ) e. A )
46 39 45 eldifd 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( f ` n ) e. ( B \ A ) )
47 difss 
 |-  ( B \ A ) C_ B
48 resmpt 
 |-  ( ( B \ A ) C_ B -> ( ( k e. B |-> C ) |` ( B \ A ) ) = ( k e. ( B \ A ) |-> C ) )
49 47 48 ax-mp 
 |-  ( ( k e. B |-> C ) |` ( B \ A ) ) = ( k e. ( B \ A ) |-> C )
50 49 fveq1i 
 |-  ( ( ( k e. B |-> C ) |` ( B \ A ) ) ` ( f ` n ) ) = ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) )
51 fvres 
 |-  ( ( f ` n ) e. ( B \ A ) -> ( ( ( k e. B |-> C ) |` ( B \ A ) ) ` ( f ` n ) ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
52 50 51 eqtr3id 
 |-  ( ( f ` n ) e. ( B \ A ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
53 46 52 syl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
54 c0ex 
 |-  0 e. _V
55 54 elsn2 
 |-  ( C e. { 0 } <-> C = 0 )
56 3 55 sylibr 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. { 0 } )
57 56 fmpttd 
 |-  ( ph -> ( k e. ( B \ A ) |-> C ) : ( B \ A ) --> { 0 } )
58 57 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( k e. ( B \ A ) |-> C ) : ( B \ A ) --> { 0 } )
59 58 46 ffvelcdmd 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) e. { 0 } )
60 elsni 
 |-  ( ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) e. { 0 } -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = 0 )
61 59 60 syl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = 0 )
62 53 61 eqtr3d 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. B |-> C ) ` ( f ` n ) ) = 0 )
63 fzssuz 
 |-  ( 1 ... ( # ` B ) ) C_ ( ZZ>= ` 1 )
64 63 a1i 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( 1 ... ( # ` B ) ) C_ ( ZZ>= ` 1 ) )
65 17 37 62 64 sumss 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> sum_ n e. ( `' f " A ) ( ( k e. B |-> C ) ` ( f ` n ) ) = sum_ n e. ( 1 ... ( # ` B ) ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
66 1 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> A C_ B )
67 66 resmptd 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> ( ( k e. B |-> C ) |` A ) = ( k e. A |-> C ) )
68 67 fveq1d 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> ( ( ( k e. B |-> C ) |` A ) ` m ) = ( ( k e. A |-> C ) ` m ) )
69 fvres 
 |-  ( m e. A -> ( ( ( k e. B |-> C ) |` A ) ` m ) = ( ( k e. B |-> C ) ` m ) )
70 69 adantl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> ( ( ( k e. B |-> C ) |` A ) ` m ) = ( ( k e. B |-> C ) ` m ) )
71 68 70 eqtr3d 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> ( ( k e. A |-> C ) ` m ) = ( ( k e. B |-> C ) ` m ) )
72 71 sumeq2dv 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> sum_ m e. A ( ( k e. A |-> C ) ` m ) = sum_ m e. A ( ( k e. B |-> C ) ` m ) )
73 fveq2 
 |-  ( m = ( f ` n ) -> ( ( k e. B |-> C ) ` m ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
74 fzfid 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( 1 ... ( # ` B ) ) e. Fin )
75 74 16 fisuppfi 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( `' f " A ) e. Fin )
76 f1of1 
 |-  ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> f : ( 1 ... ( # ` B ) ) -1-1-> B )
77 14 76 syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) -1-1-> B )
78 f1ores 
 |-  ( ( f : ( 1 ... ( # ` B ) ) -1-1-> B /\ ( `' f " A ) C_ ( 1 ... ( # ` B ) ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> ( f " ( `' f " A ) ) )
79 77 17 78 syl2anc 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> ( f " ( `' f " A ) ) )
80 f1ofo 
 |-  ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> f : ( 1 ... ( # ` B ) ) -onto-> B )
81 14 80 syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) -onto-> B )
82 1 adantr 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> A C_ B )
83 foimacnv 
 |-  ( ( f : ( 1 ... ( # ` B ) ) -onto-> B /\ A C_ B ) -> ( f " ( `' f " A ) ) = A )
84 81 82 83 syl2anc 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( f " ( `' f " A ) ) = A )
85 84 f1oeq3d 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> ( f " ( `' f " A ) ) <-> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A ) )
86 79 85 mpbid 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A )
87 fvres 
 |-  ( n e. ( `' f " A ) -> ( ( f |` ( `' f " A ) ) ` n ) = ( f ` n ) )
88 87 adantl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( `' f " A ) ) -> ( ( f |` ( `' f " A ) ) ` n ) = ( f ` n ) )
89 82 sselda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> m e. B )
90 35 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. B ) -> ( ( k e. B |-> C ) ` m ) e. CC )
91 89 90 syldan 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> ( ( k e. B |-> C ) ` m ) e. CC )
92 73 75 86 88 91 fsumf1o 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> sum_ m e. A ( ( k e. B |-> C ) ` m ) = sum_ n e. ( `' f " A ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
93 72 92 eqtrd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> sum_ m e. A ( ( k e. A |-> C ) ` m ) = sum_ n e. ( `' f " A ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
94 eqidd 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( 1 ... ( # ` B ) ) ) -> ( f ` n ) = ( f ` n ) )
95 73 74 14 94 90 fsumf1o 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> sum_ m e. B ( ( k e. B |-> C ) ` m ) = sum_ n e. ( 1 ... ( # ` B ) ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
96 65 93 95 3eqtr4d 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> sum_ m e. A ( ( k e. A |-> C ) ` m ) = sum_ m e. B ( ( k e. B |-> C ) ` m ) )
97 sumfc 
 |-  sum_ m e. A ( ( k e. A |-> C ) ` m ) = sum_ k e. A C
98 sumfc 
 |-  sum_ m e. B ( ( k e. B |-> C ) ` m ) = sum_ k e. B C
99 96 97 98 3eqtr3g 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> sum_ k e. A C = sum_ k e. B C )
100 99 expr 
 |-  ( ( ph /\ ( # ` B ) e. NN ) -> ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> sum_ k e. A C = sum_ k e. B C ) )
101 100 exlimdv 
 |-  ( ( ph /\ ( # ` B ) e. NN ) -> ( E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> sum_ k e. A C = sum_ k e. B C ) )
102 101 expimpd 
 |-  ( ph -> ( ( ( # ` B ) e. NN /\ E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) -> sum_ k e. A C = sum_ k e. B C ) )
103 fz1f1o 
 |-  ( B e. Fin -> ( B = (/) \/ ( ( # ` B ) e. NN /\ E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) )
104 4 103 syl 
 |-  ( ph -> ( B = (/) \/ ( ( # ` B ) e. NN /\ E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) )
105 12 102 104 mpjaod 
 |-  ( ph -> sum_ k e. A C = sum_ k e. B C )