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

Metamath Proof Explorer

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 ... 𝑁 ) ↦ 𝑌 ) ) )