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

Metamath Proof Explorer

Theorem gsummptfzsplitra

Description: Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the right. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummptfzsplita.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfzsplita.p ⊢ + = ( +g ‘ 𝐺 )
gsummptfzsplita.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptfzsplita.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
gsummptfzsplita.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
gsummptfzsplitra.1 ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → 𝑌 = 𝑋 )
Assertion gsummptfzsplitra ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↦ 𝑌 ) ) + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 gsummptfzsplita.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfzsplita.p ⊢ + = ( +g ‘ 𝐺 )
3 gsummptfzsplita.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptfzsplita.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 gsummptfzsplita.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑌 ∈ 𝐵 )
6 gsummptfzsplitra.1 ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → 𝑌 = 𝑋 )
7 fzfid ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
8 fzodisjsn ⊢ ( ( 𝑀 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅
9 8 a1i ⊢ ( 𝜑 → ( ( 𝑀 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ )
10 fzisfzounsn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) )
11 4 10 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) )
12 1 2 3 7 5 9 11 gsummptfidmsplit ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑁 } ↦ 𝑌 ) ) ) )
13 3 cmnmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
14 4 6 csbied ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑘 ⦌ 𝑌 = 𝑋 )
15 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
16 4 15 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
17 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝑌 ∈ 𝐵 )
18 rspcsbela ⊢ ( ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝑌 ∈ 𝐵 ) → ⦋ 𝑁 / 𝑘 ⦌ 𝑌 ∈ 𝐵 )
19 16 17 18 syl2anc ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑘 ⦌ 𝑌 ∈ 𝐵 )
20 14 19 eqeltrrd ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
21 1 13 4 20 6 gsumsnd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑁 } ↦ 𝑌 ) ) = 𝑋 )
22 21 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑁 } ↦ 𝑌 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↦ 𝑌 ) ) + 𝑋 ) )
23 12 22 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↦ 𝑌 ) ) + 𝑋 ) )