Theorem gsummptif1n0

Description: If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019) (Proof shortened by AV, 11-Oct-2019)

	Ref	Expression
Hypotheses	gsummpt1n0.0	|- .0. = ( 0g ` G )
	gsummpt1n0.g	|- ( ph -> G e. Mnd )
	gsummpt1n0.i	|- ( ph -> I e. W )
	gsummpt1n0.x	|- ( ph -> X e. I )
	gsummpt1n0.f	|- F = ( n e. I |-> if ( n = X , A , .0. ) )
	gsummptif1n0.a	|- ( ph -> A e. ( Base ` G ) )
Assertion	gsummptif1n0	|- ( ph -> ( G gsum F ) = A )

Proof

Step	Hyp	Ref	Expression
1		gsummpt1n0.0	|- .0. = ( 0g ` G )
2		gsummpt1n0.g	|- ( ph -> G e. Mnd )
3		gsummpt1n0.i	|- ( ph -> I e. W )
4		gsummpt1n0.x	|- ( ph -> X e. I )
5		gsummpt1n0.f	|- F = ( n e. I |-> if ( n = X , A , .0. ) )
6		gsummptif1n0.a	|- ( ph -> A e. ( Base ` G ) )
7	6	ralrimivw	|- ( ph -> A. n e. I A e. ( Base ` G ) )
8	1 2 3 4 5 7	gsummpt1n0	|- ( ph -> ( G gsum F ) = [_ X / n ]_ A )
9		csbconstg	|- ( X e. I -> [_ X / n ]_ A = A )
10	4 9	syl	|- ( ph -> [_ X / n ]_ A = A )
11	8 10	eqtrd	|- ( ph -> ( G gsum F ) = A )