Theorem gsumunsnd

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

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

Proof

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