Theorem gsumsnd

Description: Group sum of a singleton, deduction form. (Contributed by Thierry Arnoux, 30-Jan-2017) (Proof shortened by AV, 11-Dec-2019)

	Ref	Expression
Hypotheses	gsumsnd.b	|- B = ( Base ` G )
	gsumsnd.g	|- ( ph -> G e. Mnd )
	gsumsnd.m	|- ( ph -> M e. V )
	gsumsnd.c	|- ( ph -> C e. B )
	gsumsnd.s	|- ( ( ph /\ k = M ) -> A = C )
Assertion	gsumsnd	|- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C )

Proof

Step	Hyp	Ref	Expression
1		gsumsnd.b	|- B = ( Base ` G )
2		gsumsnd.g	|- ( ph -> G e. Mnd )
3		gsumsnd.m	|- ( ph -> M e. V )
4		gsumsnd.c	|- ( ph -> C e. B )
5		gsumsnd.s	|- ( ( ph /\ k = M ) -> A = C )
6		nfv	|- F/ k ph
7		nfcv	|- F/_ k C
8	1 2 3 4 5 6 7	gsumsnfd	|- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C )