Theorem gsumunsn

Description: Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014) (Proof shortened by AV, 8-Mar-2019)

	Ref	Expression
Hypotheses	gsumunsn.b	|- B = ( Base ` G )
	gsumunsn.p	|- .+ = ( +g ` G )
	gsumunsn.g	|- ( ph -> G e. CMnd )
	gsumunsn.a	|- ( ph -> A e. Fin )
	gsumunsn.f	|- ( ( ph /\ k e. A ) -> X e. B )
	gsumunsn.m	|- ( ph -> M e. V )
	gsumunsn.d	|- ( ph -> -. M e. A )
	gsumunsn.y	|- ( ph -> Y e. B )
	gsumunsn.s	|- ( k = M -> X = Y )
Assertion	gsumunsn	|- ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )

Proof

Step	Hyp	Ref	Expression
1		gsumunsn.b	|- B = ( Base ` G )
2		gsumunsn.p	|- .+ = ( +g ` G )
3		gsumunsn.g	|- ( ph -> G e. CMnd )
4		gsumunsn.a	|- ( ph -> A e. Fin )
5		gsumunsn.f	|- ( ( ph /\ k e. A ) -> X e. B )
6		gsumunsn.m	|- ( ph -> M e. V )
7		gsumunsn.d	|- ( ph -> -. M e. A )
8		gsumunsn.y	|- ( ph -> Y e. B )
9		gsumunsn.s	|- ( k = M -> X = Y )
10	9	adantl	|- ( ( ph /\ k = M ) -> X = Y )
11	1 2 3 4 5 6 7 8 10	gsumunsnd	|- ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )