Theorem gsummptfzsplitl

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 left. (Contributed by AV, 7-Nov-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 )
	gsummptfzsplitl.y	|- ( ( ph /\ k e. ( 0 ... N ) ) -> Y e. B )
Assertion	gsummptfzsplitl	|- ( ph -> ( G gsum ( k e. ( 0 ... N ) |-> Y ) ) = ( ( G gsum ( k e. ( 1 ... N ) |-> Y ) ) .+ ( G gsum ( k e. { 0 } |-> 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		gsummptfzsplitl.y	|- ( ( ph /\ k e. ( 0 ... N ) ) -> Y e. B )
6		fzfid	|- ( ph -> ( 0 ... N ) e. Fin )
7		incom	|- ( ( 1 ... N ) i^i { 0 } ) = ( { 0 } i^i ( 1 ... N ) )
8	7	a1i	|- ( ph -> ( ( 1 ... N ) i^i { 0 } ) = ( { 0 } i^i ( 1 ... N ) ) )
9		1e0p1	|- 1 = ( 0 + 1 )
10	9	oveq1i	|- ( 1 ... N ) = ( ( 0 + 1 ) ... N )
11	10	a1i	|- ( ph -> ( 1 ... N ) = ( ( 0 + 1 ) ... N ) )
12	11	ineq2d	|- ( ph -> ( { 0 } i^i ( 1 ... N ) ) = ( { 0 } i^i ( ( 0 + 1 ) ... N ) ) )
13		elnn0uz	|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
14	13	biimpi	|- ( N e. NN0 -> N e. ( ZZ>= ` 0 ) )
15		fzpreddisj	|- ( N e. ( ZZ>= ` 0 ) -> ( { 0 } i^i ( ( 0 + 1 ) ... N ) ) = (/) )
16	4 14 15	3syl	|- ( ph -> ( { 0 } i^i ( ( 0 + 1 ) ... N ) ) = (/) )
17	8 12 16	3eqtrd	|- ( ph -> ( ( 1 ... N ) i^i { 0 } ) = (/) )
18		fzpred	|- ( N e. ( ZZ>= ` 0 ) -> ( 0 ... N ) = ( { 0 } u. ( ( 0 + 1 ) ... N ) ) )
19	4 14 18	3syl	|- ( ph -> ( 0 ... N ) = ( { 0 } u. ( ( 0 + 1 ) ... N ) ) )
20		uncom	|- ( { 0 } u. ( ( 0 + 1 ) ... N ) ) = ( ( ( 0 + 1 ) ... N ) u. { 0 } )
21		0p1e1	|- ( 0 + 1 ) = 1
22	21	oveq1i	|- ( ( 0 + 1 ) ... N ) = ( 1 ... N )
23	22	uneq1i	|- ( ( ( 0 + 1 ) ... N ) u. { 0 } ) = ( ( 1 ... N ) u. { 0 } )
24	20 23	eqtri	|- ( { 0 } u. ( ( 0 + 1 ) ... N ) ) = ( ( 1 ... N ) u. { 0 } )
25	19 24	syl6eq	|- ( ph -> ( 0 ... N ) = ( ( 1 ... N ) u. { 0 } ) )
26	1 2 3 6 5 17 25	gsummptfidmsplit	|- ( ph -> ( G gsum ( k e. ( 0 ... N ) |-> Y ) ) = ( ( G gsum ( k e. ( 1 ... N ) |-> Y ) ) .+ ( G gsum ( k e. { 0 } |-> Y ) ) ) )