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 φ A B
sumss.2 φ k A C
sumss.3 φ k B A C = 0
fsumss.4 φ B Fin
Assertion fsumss φ k A C = k B C

Proof

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