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 φ A Fin
gsumfsum.2 φ k A B
Assertion gsumfsum φ fld k A B = k A B

Proof

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