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

Metamath Proof Explorer

Theorem gsummptfzsplit

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 AV, 25-Oct-2019)

Ref Expression
Hypotheses gsummptfzsplit.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptfzsplit.p ⊢ + = ( +g ‘ 𝐺 )
gsummptfzsplit.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptfzsplit.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
gsummptfzsplit.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑌 ∈ 𝐵 )
Assertion gsummptfzsplit ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptfzsplit.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptfzsplit.p ⊢ + = ( +g ‘ 𝐺 )
3 gsummptfzsplit.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptfzsplit.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 gsummptfzsplit.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑌 ∈ 𝐵 )
6 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
7 fzp1disj ⊢ ( ( 0 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅
8 7 a1i ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ )
9 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
10 4 9 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
11 fzsuc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... ( 𝑁 + 1 ) ) = ( ( 0 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
12 10 11 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) = ( ( 0 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
13 1 2 3 6 5 8 12 gsummptfidmsplit ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { ( 𝑁 + 1 ) } ↦ 𝑌 ) ) ) )