Metamath Proof Explorer

Theorem gsumfsum

Description: Relate a group sum on CCfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses gsumfsum.1 
|- ( ph -> A e. Fin )
gsumfsum.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion gsumfsum 
|- ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 gsumfsum.1 
 |-  ( ph -> A e. Fin )
2 gsumfsum.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 mpteq1 
 |-  ( A = (/) -> ( k e. A |-> B ) = ( k e. (/) |-> B ) )
4 mpt0 
 |-  ( k e. (/) |-> B ) = (/)
5 3 4 eqtrdi 
 |-  ( A = (/) -> ( k e. A |-> B ) = (/) )
6 5 oveq2d 
 |-  ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = ( CCfld gsum (/) ) )
7 cnfld0 
 |-  0 = ( 0g ` CCfld )
8 7 gsum0 
 |-  ( CCfld gsum (/) ) = 0
9 sum0 
 |-  sum_ k e. (/) B = 0
10 8 9 eqtr4i 
 |-  ( CCfld gsum (/) ) = sum_ k e. (/) B
11 6 10 eqtrdi 
 |-  ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. (/) B )
12 sumeq1 
 |-  ( A = (/) -> sum_ k e. A B = sum_ k e. (/) B )
13 11 12 eqtr4d 
 |-  ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B )
14 13 a1i 
 |-  ( ph -> ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) )
15 cnfldbas 
 |-  CC = ( Base ` CCfld )
16 cnfldadd 
 |-  + = ( +g ` CCfld )
17 eqid 
 |-  ( Cntz ` CCfld ) = ( Cntz ` CCfld )
18 cnring 
 |-  CCfld e. Ring
19 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
20 18 19 mp1i 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> CCfld e. Mnd )
21 1 adantr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> A e. Fin )
22 2 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
23 22 adantr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> B ) : A --> CC )
24 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
25 18 24 mp1i 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> CCfld e. CMnd )
26 15 17 25 23 cntzcmnf 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ran ( k e. A |-> B ) C_ ( ( Cntz ` CCfld ) ` ran ( k e. A |-> B ) ) )
27 simprl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
28 simprr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
29 f1of1 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) -1-1-> A )
30 28 29 syl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-> A )
31 suppssdm 
 |-  ( ( k e. A |-> B ) supp 0 ) C_ dom ( k e. A |-> B )
32 31 23 fssdm 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) supp 0 ) C_ A )
33 f1ofo 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) -onto-> A )
34 forn 
 |-  ( f : ( 1 ... ( # ` A ) ) -onto-> A -> ran f = A )
35 28 33 34 3syl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ran f = A )
36 32 35 sseqtrrd 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) supp 0 ) C_ ran f )
37 eqid 
 |-  ( ( ( k e. A |-> B ) o. f ) supp 0 ) = ( ( ( k e. A |-> B ) o. f ) supp 0 )
38 15 7 16 17 20 21 23 26 27 30 36 37 gsumval3 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( CCfld gsum ( k e. A |-> B ) ) = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
39 sumfc 
 |-  sum_ x e. A ( ( k e. A |-> B ) ` x ) = sum_ k e. A B
40 fveq2 
 |-  ( x = ( f ` n ) -> ( ( k e. A |-> B ) ` x ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
41 23 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. A ) -> ( ( k e. A |-> B ) ` x ) e. CC )
42 f1of 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
43 28 42 syl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
44 fvco3 
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
45 43 44 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 ) ) )
46 40 27 28 41 45 fsum 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ x e. A ( ( k e. A |-> B ) ` x ) = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
47 39 46 eqtr3id 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ k e. A B = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
48 38 47 eqtr4d 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B )
49 48 expr 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) )
50 49 exlimdv 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) )
51 50 expimpd 
 |-  ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) )
52 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
53 1 52 syl 
 |-  ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
54 14 51 53 mpjaod 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B )