Metamath Proof Explorer

Theorem fsumrelem

Description: Lemma for fsumre , fsumim , and fsumcj . (Contributed by Mario Carneiro, 25-Jul-2014) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses fsumre.1 
|- ( ph -> A e. Fin )
fsumre.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
fsumrelem.3 
|- F : CC --> CC
fsumrelem.4 
|- ( ( x e. CC /\ y e. CC ) -> ( F ` ( x + y ) ) = ( ( F ` x ) + ( F ` y ) ) )
Assertion fsumrelem 
|- ( ph -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) )

Proof

Step Hyp Ref Expression
1 fsumre.1 
 |-  ( ph -> A e. Fin )
2 fsumre.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 fsumrelem.3 
 |-  F : CC --> CC
4 fsumrelem.4 
 |-  ( ( x e. CC /\ y e. CC ) -> ( F ` ( x + y ) ) = ( ( F ` x ) + ( F ` y ) ) )
5 0cn 
 |-  0 e. CC
6 3 ffvelrni 
 |-  ( 0 e. CC -> ( F ` 0 ) e. CC )
7 5 6 ax-mp 
 |-  ( F ` 0 ) e. CC
8 7 addid1i 
 |-  ( ( F ` 0 ) + 0 ) = ( F ` 0 )
9 fvoveq1 
 |-  ( x = 0 -> ( F ` ( x + y ) ) = ( F ` ( 0 + y ) ) )
10 fveq2 
 |-  ( x = 0 -> ( F ` x ) = ( F ` 0 ) )
11 10 oveq1d 
 |-  ( x = 0 -> ( ( F ` x ) + ( F ` y ) ) = ( ( F ` 0 ) + ( F ` y ) ) )
12 9 11 eqeq12d 
 |-  ( x = 0 -> ( ( F ` ( x + y ) ) = ( ( F ` x ) + ( F ` y ) ) <-> ( F ` ( 0 + y ) ) = ( ( F ` 0 ) + ( F ` y ) ) ) )
13 oveq2 
 |-  ( y = 0 -> ( 0 + y ) = ( 0 + 0 ) )
14 00id 
 |-  ( 0 + 0 ) = 0
15 13 14 eqtrdi 
 |-  ( y = 0 -> ( 0 + y ) = 0 )
16 15 fveq2d 
 |-  ( y = 0 -> ( F ` ( 0 + y ) ) = ( F ` 0 ) )
17 fveq2 
 |-  ( y = 0 -> ( F ` y ) = ( F ` 0 ) )
18 17 oveq2d 
 |-  ( y = 0 -> ( ( F ` 0 ) + ( F ` y ) ) = ( ( F ` 0 ) + ( F ` 0 ) ) )
19 16 18 eqeq12d 
 |-  ( y = 0 -> ( ( F ` ( 0 + y ) ) = ( ( F ` 0 ) + ( F ` y ) ) <-> ( F ` 0 ) = ( ( F ` 0 ) + ( F ` 0 ) ) ) )
20 12 19 4 vtocl2ga 
 |-  ( ( 0 e. CC /\ 0 e. CC ) -> ( F ` 0 ) = ( ( F ` 0 ) + ( F ` 0 ) ) )
21 5 5 20 mp2an 
 |-  ( F ` 0 ) = ( ( F ` 0 ) + ( F ` 0 ) )
22 8 21 eqtr2i 
 |-  ( ( F ` 0 ) + ( F ` 0 ) ) = ( ( F ` 0 ) + 0 )
23 7 7 5 addcani 
 |-  ( ( ( F ` 0 ) + ( F ` 0 ) ) = ( ( F ` 0 ) + 0 ) <-> ( F ` 0 ) = 0 )
24 22 23 mpbi 
 |-  ( F ` 0 ) = 0
25 sumeq1 
 |-  ( A = (/) -> sum_ k e. A B = sum_ k e. (/) B )
26 sum0 
 |-  sum_ k e. (/) B = 0
27 25 26 eqtrdi 
 |-  ( A = (/) -> sum_ k e. A B = 0 )
28 27 fveq2d 
 |-  ( A = (/) -> ( F ` sum_ k e. A B ) = ( F ` 0 ) )
29 sumeq1 
 |-  ( A = (/) -> sum_ k e. A ( F ` B ) = sum_ k e. (/) ( F ` B ) )
30 sum0 
 |-  sum_ k e. (/) ( F ` B ) = 0
31 29 30 eqtrdi 
 |-  ( A = (/) -> sum_ k e. A ( F ` B ) = 0 )
32 24 28 31 3eqtr4a 
 |-  ( A = (/) -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) )
33 32 a1i 
 |-  ( ph -> ( A = (/) -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) ) )
34 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
35 34 adantl 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
36 2 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
37 36 adantr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> B ) : A --> CC )
38 simprr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
39 f1of 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
40 38 39 syl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
41 fco 
 |-  ( ( ( k e. A |-> B ) : A --> CC /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
42 37 40 41 syl2anc 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
43 42 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) e. CC )
44 simprl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
45 nnuz 
 |-  NN = ( ZZ>= ` 1 )
46 44 45 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) )
47 4 adantl 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ ( x e. CC /\ y e. CC ) ) -> ( F ` ( x + y ) ) = ( ( F ` x ) + ( F ` y ) ) )
48 40 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( f ` x ) e. A )
49 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
50 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
51 50 fvmpt2 
 |-  ( ( k e. A /\ B e. CC ) -> ( ( k e. A |-> B ) ` k ) = B )
52 49 2 51 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> B ) ` k ) = B )
53 52 fveq2d 
 |-  ( ( ph /\ k e. A ) -> ( F ` ( ( k e. A |-> B ) ` k ) ) = ( F ` B ) )
54 fvex 
 |-  ( F ` B ) e. _V
55 eqid 
 |-  ( k e. A |-> ( F ` B ) ) = ( k e. A |-> ( F ` B ) )
56 55 fvmpt2 
 |-  ( ( k e. A /\ ( F ` B ) e. _V ) -> ( ( k e. A |-> ( F ` B ) ) ` k ) = ( F ` B ) )
57 49 54 56 sylancl 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> ( F ` B ) ) ` k ) = ( F ` B ) )
58 53 57 eqtr4d 
 |-  ( ( ph /\ k e. A ) -> ( F ` ( ( k e. A |-> B ) ` k ) ) = ( ( k e. A |-> ( F ` B ) ) ` k ) )
59 58 ralrimiva 
 |-  ( ph -> A. k e. A ( F ` ( ( k e. A |-> B ) ` k ) ) = ( ( k e. A |-> ( F ` B ) ) ` k ) )
60 59 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> A. k e. A ( F ` ( ( k e. A |-> B ) ` k ) ) = ( ( k e. A |-> ( F ` B ) ) ` k ) )
61 nfcv 
 |-  F/_ k F
62 nffvmpt1 
 |-  F/_ k ( ( k e. A |-> B ) ` ( f ` x ) )
63 61 62 nffv 
 |-  F/_ k ( F ` ( ( k e. A |-> B ) ` ( f ` x ) ) )
64 nffvmpt1 
 |-  F/_ k ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) )
65 63 64 nfeq 
 |-  F/ k ( F ` ( ( k e. A |-> B ) ` ( f ` x ) ) ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) )
66 2fveq3 
 |-  ( k = ( f ` x ) -> ( F ` ( ( k e. A |-> B ) ` k ) ) = ( F ` ( ( k e. A |-> B ) ` ( f ` x ) ) ) )
67 fveq2 
 |-  ( k = ( f ` x ) -> ( ( k e. A |-> ( F ` B ) ) ` k ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) ) )
68 66 67 eqeq12d 
 |-  ( k = ( f ` x ) -> ( ( F ` ( ( k e. A |-> B ) ` k ) ) = ( ( k e. A |-> ( F ` B ) ) ` k ) <-> ( F ` ( ( k e. A |-> B ) ` ( f ` x ) ) ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) ) ) )
69 65 68 rspc 
 |-  ( ( f ` x ) e. A -> ( A. k e. A ( F ` ( ( k e. A |-> B ) ` k ) ) = ( ( k e. A |-> ( F ` B ) ) ` k ) -> ( F ` ( ( k e. A |-> B ) ` ( f ` x ) ) ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) ) ) )
70 48 60 69 sylc 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( F ` ( ( k e. A |-> B ) ` ( f ` x ) ) ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) ) )
71 fvco3 
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
72 40 71 sylan 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
73 72 fveq2d 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( F ` ( ( ( k e. A |-> B ) o. f ) ` x ) ) = ( F ` ( ( k e. A |-> B ) ` ( f ` x ) ) ) )
74 fvco3 
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( F ` B ) ) o. f ) ` x ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) ) )
75 40 74 sylan 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( F ` B ) ) o. f ) ` x ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) ) )
76 70 73 75 3eqtr4d 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( F ` ( ( ( k e. A |-> B ) o. f ) ` x ) ) = ( ( ( k e. A |-> ( F ` B ) ) o. f ) ` x ) )
77 35 43 46 47 76 seqhomo 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( F ` ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) = ( seq 1 ( + , ( ( k e. A |-> ( F ` B ) ) o. f ) ) ` ( # ` A ) ) )
78 fveq2 
 |-  ( m = ( f ` x ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
79 37 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
80 78 44 38 79 72 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 ) ) )
81 80 fveq2d 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( F ` sum_ m e. A ( ( k e. A |-> B ) ` m ) ) = ( F ` ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) )
82 fveq2 
 |-  ( m = ( f ` x ) -> ( ( k e. A |-> ( F ` B ) ) ` m ) = ( ( k e. A |-> ( F ` B ) ) ` ( f ` x ) ) )
83 3 ffvelrni 
 |-  ( B e. CC -> ( F ` B ) e. CC )
84 2 83 syl 
 |-  ( ( ph /\ k e. A ) -> ( F ` B ) e. CC )
85 84 fmpttd 
 |-  ( ph -> ( k e. A |-> ( F ` B ) ) : A --> CC )
86 85 adantr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> ( F ` B ) ) : A --> CC )
87 86 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> ( F ` B ) ) ` m ) e. CC )
88 82 44 38 87 75 fsum 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ m e. A ( ( k e. A |-> ( F ` B ) ) ` m ) = ( seq 1 ( + , ( ( k e. A |-> ( F ` B ) ) o. f ) ) ` ( # ` A ) ) )
89 77 81 88 3eqtr4d 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( F ` sum_ m e. A ( ( k e. A |-> B ) ` m ) ) = sum_ m e. A ( ( k e. A |-> ( F ` B ) ) ` m ) )
90 sumfc 
 |-  sum_ m e. A ( ( k e. A |-> B ) ` m ) = sum_ k e. A B
91 90 fveq2i 
 |-  ( F ` sum_ m e. A ( ( k e. A |-> B ) ` m ) ) = ( F ` sum_ k e. A B )
92 sumfc 
 |-  sum_ m e. A ( ( k e. A |-> ( F ` B ) ) ` m ) = sum_ k e. A ( F ` B )
93 89 91 92 3eqtr3g 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) )
94 93 expr 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) ) )
95 94 exlimdv 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) ) )
96 95 expimpd 
 |-  ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) ) )
97 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
98 1 97 syl 
 |-  ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
99 33 96 98 mpjaod 
 |-  ( ph -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) )