Metamath Proof Explorer

Theorem fsumadd

Description: The sum of two finite sums. (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumadd.1 
|- ( ph -> A e. Fin )
fsumadd.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
fsumadd.3 
|- ( ( ph /\ k e. A ) -> C e. CC )
Assertion fsumadd 
|- ( ph -> sum_ k e. A ( B + C ) = ( sum_ k e. A B + sum_ k e. A C ) )

Proof

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