Theorem gsummulg

Description: Nonnegative multiple of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 7-Jan-2015) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsummulg.b	|- B = ( Base ` G )
	gsummulg.z	|- .0. = ( 0g ` G )
	gsummulg.t	|- .x. = ( .g ` G )
	gsummulg.a	|- ( ph -> A e. V )
	gsummulg.f	|- ( ( ph /\ k e. A ) -> X e. B )
	gsummulg.w	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
	gsummulg.g	|- ( ph -> G e. CMnd )
	gsummulg.n	|- ( ph -> N e. NN0 )
Assertion	gsummulg	|- ( ph -> ( G gsum ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsum ( k e. A |-> X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummulg.b	|- B = ( Base ` G )
2		gsummulg.z	|- .0. = ( 0g ` G )
3		gsummulg.t	|- .x. = ( .g ` G )
4		gsummulg.a	|- ( ph -> A e. V )
5		gsummulg.f	|- ( ( ph /\ k e. A ) -> X e. B )
6		gsummulg.w	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
7		gsummulg.g	|- ( ph -> G e. CMnd )
8		gsummulg.n	|- ( ph -> N e. NN0 )
9	8	nn0zd	|- ( ph -> N e. ZZ )
10	8	olcd	|- ( ph -> ( G e. Abel \/ N e. NN0 ) )
11	1 2 3 4 5 6 7 9 10	gsummulglem	|- ( ph -> ( G gsum ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsum ( k e. A |-> X ) ) ) )