This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝐴 𝐵 )