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	|- B = ( Base ` G )
	gsummptfzsplit.p	|- .+ = ( +g ` G )
	gsummptfzsplit.g	|- ( ph -> G e. CMnd )
	gsummptfzsplit.n	|- ( ph -> N e. NN0 )
	gsummptfzsplit.y	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> Y e. B )
Assertion	gsummptfzsplit	|- ( ph -> ( G gsum ( k e. ( 0 ... ( N + 1 ) ) |-> Y ) ) = ( ( G gsum ( k e. ( 0 ... N ) |-> Y ) ) .+ ( G gsum ( k e. { ( N + 1 ) } |-> Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfzsplit.b	|- B = ( Base ` G )
2		gsummptfzsplit.p	|- .+ = ( +g ` G )
3		gsummptfzsplit.g	|- ( ph -> G e. CMnd )
4		gsummptfzsplit.n	|- ( ph -> N e. NN0 )
5		gsummptfzsplit.y	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> Y e. B )
6		fzfid	|- ( ph -> ( 0 ... ( N + 1 ) ) e. Fin )
7		fzp1disj	|- ( ( 0 ... N ) i^i { ( N + 1 ) } ) = (/)
8	7	a1i	|- ( ph -> ( ( 0 ... N ) i^i { ( N + 1 ) } ) = (/) )
9		elnn0uz	|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
10	4 9	sylib	|- ( ph -> N e. ( ZZ>= ` 0 ) )
11		fzsuc	|- ( N e. ( ZZ>= ` 0 ) -> ( 0 ... ( N + 1 ) ) = ( ( 0 ... N ) u. { ( N + 1 ) } ) )
12	10 11	syl	|- ( ph -> ( 0 ... ( N + 1 ) ) = ( ( 0 ... N ) u. { ( N + 1 ) } ) )
13	1 2 3 6 5 8 12	gsummptfidmsplit	|- ( ph -> ( G gsum ( k e. ( 0 ... ( N + 1 ) ) |-> Y ) ) = ( ( G gsum ( k e. ( 0 ... N ) |-> Y ) ) .+ ( G gsum ( k e. { ( N + 1 ) } |-> Y ) ) ) )