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	\|- 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 ) ) ) )