Theorem gsumsnfd

Description: Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Revised 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 )
	gsumsnfd.p	|- F/ k ph
	gsumsnfd.c	|- F/_ k C
Assertion	gsumsnfd	|- ( 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		gsumsnfd.p	|- F/ k ph
7		gsumsnfd.c	|- F/_ k C
8		elsni	|- ( k e. { M } -> k = M )
9	8 5	sylan2	|- ( ( ph /\ k e. { M } ) -> A = C )
10	6 9	mpteq2da	|- ( ph -> ( k e. { M } |-> A ) = ( k e. { M } |-> C ) )
11	10	oveq2d	|- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = ( G gsum ( k e. { M } |-> C ) ) )
12		snfi	|- { M } e. Fin
13	12	a1i	|- ( ph -> { M } e. Fin )
14		eqid	|- ( .g ` G ) = ( .g ` G )
15	7 1 14	gsumconstf	|- ( ( G e. Mnd /\ { M } e. Fin /\ C e. B ) -> ( G gsum ( k e. { M } |-> C ) ) = ( ( # ` { M } ) ( .g ` G ) C ) )
16	2 13 4 15	syl3anc	|- ( ph -> ( G gsum ( k e. { M } |-> C ) ) = ( ( # ` { M } ) ( .g ` G ) C ) )
17	11 16	eqtrd	|- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = ( ( # ` { M } ) ( .g ` G ) C ) )
18		hashsng	|- ( M e. V -> ( # ` { M } ) = 1 )
19	3 18	syl	|- ( ph -> ( # ` { M } ) = 1 )
20	19	oveq1d	|- ( ph -> ( ( # ` { M } ) ( .g ` G ) C ) = ( 1 ( .g ` G ) C ) )
21	1 14	mulg1	|- ( C e. B -> ( 1 ( .g ` G ) C ) = C )
22	4 21	syl	|- ( ph -> ( 1 ( .g ` G ) C ) = C )
23	17 20 22	3eqtrd	|- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C )