Theorem gsumunsnf

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)

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

Proof

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