Theorem gsummptp1

Description: Reindex a zero-based sum as a one-base sum. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	gsummptp1.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	gsummptp1.2	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	gsummptp1.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	gsummptp1.4	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
	gsummptp1.5	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑙 = ( 𝑘 + 1 ) ) → 𝑌 = 𝑋 )
Assertion	gsummptp1	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑋 ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 1 ... 𝑁 ) ↦ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptp1.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		gsummptp1.2	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
3		gsummptp1.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		gsummptp1.4	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
5		gsummptp1.5	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑙 = ( 𝑘 + 1 ) ) → 𝑌 = 𝑋 )
6		nfcsb1v	⊢ Ⅎ 𝑙 ⦋ ( 𝑘 + 1 ) / 𝑙 ⦌ 𝑌
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8		csbeq1a	⊢ ( 𝑙 = ( 𝑘 + 1 ) → 𝑌 = ⦋ ( 𝑘 + 1 ) / 𝑙 ⦌ 𝑌 )
9		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
10		ssidd	⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
11		fz0add1fz1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝑁 ) )
12	3 11	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝑁 ) )
13		fz1fzo0m1	⊢ ( 𝑙 ∈ ( 1 ... 𝑁 ) → ( 𝑙 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) → ( 𝑙 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
15		eqcom	⊢ ( ( 𝑘 + 1 ) = 𝑙 ↔ 𝑙 = ( 𝑘 + 1 ) )
16		elfzonn0	⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℕ0 )
17	16	adantl	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
18	17	nn0cnd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℂ )
19		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ ℂ )
20		elfznn	⊢ ( 𝑙 ∈ ( 1 ... 𝑁 ) → 𝑙 ∈ ℕ )
21	20	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑙 ∈ ℕ )
22	21	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑙 ∈ ℂ )
23	18 19 22	addlsub	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑘 + 1 ) = 𝑙 ↔ 𝑘 = ( 𝑙 − 1 ) ) )
24	15 23	bitr3id	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑙 = ( 𝑘 + 1 ) ↔ 𝑘 = ( 𝑙 − 1 ) ) )
25	14 24	reu6dv	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 1 ... 𝑁 ) ) → ∃! 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑙 = ( 𝑘 + 1 ) )
26	6 1 7 8 2 9 10 4 12 25	gsummptf1o	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑙 ∈ ( 1 ... 𝑁 ) ↦ 𝑌 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ⦋ ( 𝑘 + 1 ) / 𝑙 ⦌ 𝑌 ) ) )
27	12 5	csbied	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑙 ⦌ 𝑌 = 𝑋 )
28	27	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ⦋ ( 𝑘 + 1 ) / 𝑙 ⦌ 𝑌 ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑋 ) )
29	28	oveq2d	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ⦋ ( 𝑘 + 1 ) / 𝑙 ⦌ 𝑌 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑋 ) ) )
30	26 29	eqtr2d	⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑋 ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 1 ... 𝑁 ) ↦ 𝑌 ) ) )