Theorem gsumzrsum

Description: Relate a group sum on ZZring to a finite sum on the complex numbers. See also gsumfsum . (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	gsumzrsum.1	|- ( ph -> A e. Fin )
	gsumzrsum.2	|- ( ( ph /\ k e. A ) -> B e. ZZ )
Assertion	gsumzrsum	|- ( ph -> ( ZZring gsum ( k e. A |-> B ) ) = sum_ k e. A B )

Proof

Step	Hyp	Ref	Expression
1		gsumzrsum.1	|- ( ph -> A e. Fin )
2		gsumzrsum.2	|- ( ( ph /\ k e. A ) -> B e. ZZ )
3		cnfldbas	|- CC = ( Base ` CCfld )
4		cnfldadd	|- + = ( +g ` CCfld )
5		df-zring	|- ZZring = ( CCfld |`s ZZ )
6		cnfldex	|- CCfld e. _V
7	6	a1i	|- ( ph -> CCfld e. _V )
8		zsscn	|- ZZ C_ CC
9	8	a1i	|- ( ph -> ZZ C_ CC )
10	2	fmpttd	|- ( ph -> ( k e. A |-> B ) : A --> ZZ )
11		0zd	|- ( ph -> 0 e. ZZ )
12		addlid	|- ( k e. CC -> ( 0 + k ) = k )
13		addrid	|- ( k e. CC -> ( k + 0 ) = k )
14	12 13	jca	|- ( k e. CC -> ( ( 0 + k ) = k /\ ( k + 0 ) = k ) )
15	14	adantl	|- ( ( ph /\ k e. CC ) -> ( ( 0 + k ) = k /\ ( k + 0 ) = k ) )
16	3 4 5 7 1 9 10 11 15	gsumress	|- ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = ( ZZring gsum ( k e. A |-> B ) ) )
17	2	zcnd	|- ( ( ph /\ k e. A ) -> B e. CC )
18	1 17	gsumfsum	|- ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B )
19	16 18	eqtr3d	|- ( ph -> ( ZZring gsum ( k e. A |-> B ) ) = sum_ k e. A B )