Metamath Proof Explorer


Theorem fsummulc2

Description: A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsummulc2.1 φ A Fin
fsummulc2.2 φ C
fsummulc2.3 φ k A B
Assertion fsummulc2 φ C k A B = k A C B

Proof

Step Hyp Ref Expression
1 fsummulc2.1 φ A Fin
2 fsummulc2.2 φ C
3 fsummulc2.3 φ k A B
4 2 mul01d φ C 0 = 0
5 sumeq1 A = k A B = k B
6 sum0 k B = 0
7 5 6 eqtrdi A = k A B = 0
8 7 oveq2d A = C k A B = C 0
9 sumeq1 A = k A C B = k C B
10 sum0 k C B = 0
11 9 10 eqtrdi A = k A C B = 0
12 8 11 eqeq12d A = C k A B = k A C B C 0 = 0
13 4 12 syl5ibrcom φ A = C k A B = k A C B
14 addcl n m n + m
15 14 adantl φ A f : 1 A 1-1 onto A n m n + m
16 2 adantr φ A f : 1 A 1-1 onto A C
17 adddi C n m C n + m = C n + C m
18 17 3expb C n m C n + m = C n + C m
19 16 18 sylan φ A f : 1 A 1-1 onto A n m C n + m = C n + C m
20 simprl φ A f : 1 A 1-1 onto A A
21 nnuz = 1
22 20 21 eleqtrdi φ A f : 1 A 1-1 onto A A 1
23 3 fmpttd φ k A B : A
24 23 ad2antrr φ A f : 1 A 1-1 onto A n 1 A k A B : A
25 simprr φ A f : 1 A 1-1 onto A f : 1 A 1-1 onto A
26 25 adantr φ A f : 1 A 1-1 onto A n 1 A f : 1 A 1-1 onto A
27 f1of f : 1 A 1-1 onto A f : 1 A A
28 26 27 syl φ A f : 1 A 1-1 onto A n 1 A f : 1 A A
29 fco k A B : A f : 1 A A k A B f : 1 A
30 24 28 29 syl2anc φ A f : 1 A 1-1 onto A n 1 A k A B f : 1 A
31 simpr φ A f : 1 A 1-1 onto A n 1 A n 1 A
32 30 31 ffvelrnd φ A f : 1 A 1-1 onto A n 1 A k A B f n
33 28 31 ffvelrnd φ A f : 1 A 1-1 onto A n 1 A f n A
34 simpr φ k A k A
35 2 adantr φ k A C
36 35 3 mulcld φ k A C B
37 eqid k A C B = k A C B
38 37 fvmpt2 k A C B k A C B k = C B
39 34 36 38 syl2anc φ k A k A C B k = C B
40 eqid k A B = k A B
41 40 fvmpt2 k A B k A B k = B
42 34 3 41 syl2anc φ k A k A B k = B
43 42 oveq2d φ k A C k A B k = C B
44 39 43 eqtr4d φ k A k A C B k = C k A B k
45 44 ralrimiva φ k A k A C B k = C k A B k
46 45 ad2antrr φ A f : 1 A 1-1 onto A n 1 A k A k A C B k = C k A B k
47 nffvmpt1 _ k k A C B f n
48 nfcv _ k C
49 nfcv _ k ×
50 nffvmpt1 _ k k A B f n
51 48 49 50 nfov _ k C k A B f n
52 47 51 nfeq k k A C B f n = C k A B f n
53 fveq2 k = f n k A C B k = k A C B f n
54 fveq2 k = f n k A B k = k A B f n
55 54 oveq2d k = f n C k A B k = C k A B f n
56 53 55 eqeq12d k = f n k A C B k = C k A B k k A C B f n = C k A B f n
57 52 56 rspc f n A k A k A C B k = C k A B k k A C B f n = C k A B f n
58 33 46 57 sylc φ A f : 1 A 1-1 onto A n 1 A k A C B f n = C k A B f n
59 27 ad2antll φ A f : 1 A 1-1 onto A f : 1 A A
60 fvco3 f : 1 A A n 1 A k A C B f n = k A C B f n
61 59 60 sylan φ A f : 1 A 1-1 onto A n 1 A k A C B f n = k A C B f n
62 fvco3 f : 1 A A n 1 A k A B f n = k A B f n
63 59 62 sylan φ A f : 1 A 1-1 onto A n 1 A k A B f n = k A B f n
64 63 oveq2d φ A f : 1 A 1-1 onto A n 1 A C k A B f n = C k A B f n
65 58 61 64 3eqtr4d φ A f : 1 A 1-1 onto A n 1 A k A C B f n = C k A B f n
66 15 19 22 32 65 seqdistr φ A f : 1 A 1-1 onto A seq 1 + k A C B f A = C seq 1 + k A B f A
67 fveq2 m = f n k A C B m = k A C B f n
68 36 fmpttd φ k A C B : A
69 68 adantr φ A f : 1 A 1-1 onto A k A C B : A
70 69 ffvelrnda φ A f : 1 A 1-1 onto A m A k A C B m
71 67 20 25 70 61 fsum φ A f : 1 A 1-1 onto A m A k A C B m = seq 1 + k A C B f A
72 fveq2 m = f n k A B m = k A B f n
73 23 adantr φ A f : 1 A 1-1 onto A k A B : A
74 73 ffvelrnda φ A f : 1 A 1-1 onto A m A k A B m
75 72 20 25 74 63 fsum φ A f : 1 A 1-1 onto A m A k A B m = seq 1 + k A B f A
76 75 oveq2d φ A f : 1 A 1-1 onto A C m A k A B m = C seq 1 + k A B f A
77 66 71 76 3eqtr4rd φ A f : 1 A 1-1 onto A C m A k A B m = m A k A C B m
78 sumfc m A k A B m = k A B
79 78 oveq2i C m A k A B m = C k A B
80 sumfc m A k A C B m = k A C B
81 77 79 80 3eqtr3g φ A f : 1 A 1-1 onto A C k A B = k A C B
82 81 expr φ A f : 1 A 1-1 onto A C k A B = k A C B
83 82 exlimdv φ A f f : 1 A 1-1 onto A C k A B = k A C B
84 83 expimpd φ A f f : 1 A 1-1 onto A C k A B = k A C B
85 fz1f1o A Fin A = A f f : 1 A 1-1 onto A
86 1 85 syl φ A = A f f : 1 A 1-1 onto A
87 13 84 86 mpjaod φ C k A B = k A C B