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 
|- ( ph -> A e. Fin )
fsummulc2.2 
|- ( ph -> C e. CC )
fsummulc2.3 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsummulc2 
|- ( ph -> ( C x. sum_ k e. A B ) = sum_ k e. A ( C x. B ) )

Proof

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