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 ffvelrnda
 |-  ( ( ( 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 )