Theorem gsumsnf

Description: Group sum of a singleton, 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	gsumsnf.c	|- F/_ k C
	gsumsnf.b	|- B = ( Base ` G )
	gsumsnf.s	|- ( k = M -> A = C )
Assertion	gsumsnf	|- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsum ( k e. { M } |-> A ) ) = C )

Proof

Step	Hyp	Ref	Expression
1		gsumsnf.c	|- F/_ k C
2		gsumsnf.b	|- B = ( Base ` G )
3		gsumsnf.s	|- ( k = M -> A = C )
4		simp1	|- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> G e. Mnd )
5		simp2	|- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> M e. V )
6		simp3	|- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> C e. B )
7	3	adantl	|- ( ( ( G e. Mnd /\ M e. V /\ C e. B ) /\ k = M ) -> A = C )
8		nfv	|- F/ k G e. Mnd
9		nfv	|- F/ k M e. V
10	1	nfel1	|- F/ k C e. B
11	8 9 10	nf3an	|- F/ k ( G e. Mnd /\ M e. V /\ C e. B )
12	2 4 5 6 7 11 1	gsumsnfd	|- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsum ( k e. { M } |-> A ) ) = C )