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 ) } ↦ 𝑌 ) ) ) )