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	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsumzrsum.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
Assertion	gsumzrsum	⊢ ( 𝜑 → ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		gsumzrsum.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		gsumzrsum.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℤ )
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4		cnfldadd	⊢ + = ( +g ‘ ℂfld )
5		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
6		cnfldex	⊢ ℂfld ∈ V
7	6	a1i	⊢ ( 𝜑 → ℂfld ∈ V )
8		zsscn	⊢ ℤ ⊆ ℂ
9	8	a1i	⊢ ( 𝜑 → ℤ ⊆ ℂ )
10	2	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℤ )
11		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
12		addlid	⊢ ( 𝑘 ∈ ℂ → ( 0 + 𝑘 ) = 𝑘 )
13		addrid	⊢ ( 𝑘 ∈ ℂ → ( 𝑘 + 0 ) = 𝑘 )
14	12 13	jca	⊢ ( 𝑘 ∈ ℂ → ( ( 0 + 𝑘 ) = 𝑘 ∧ ( 𝑘 + 0 ) = 𝑘 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℂ ) → ( ( 0 + 𝑘 ) = 𝑘 ∧ ( 𝑘 + 0 ) = 𝑘 ) )
16	3 4 5 7 1 9 10 11 15	gsumress	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
17	2	zcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
18	1 17	gsumfsum	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )
19	16 18	eqtr3d	⊢ ( 𝜑 → ( ℤring Σg ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )