Theorem gsummulgz

Description: Integer multiple of a group sum. (Contributed 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. )
	gsummulgz.g	|- ( ph -> G e. Abel )
	gsummulgz.n	|- ( ph -> N e. ZZ )
Assertion	gsummulgz	|- ( 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		gsummulgz.g	|- ( ph -> G e. Abel )
8		gsummulgz.n	|- ( ph -> N e. ZZ )
9		ablcmn	|- ( G e. Abel -> G e. CMnd )
10	7 9	syl	|- ( ph -> G e. CMnd )
11	7	orcd	|- ( ph -> ( G e. Abel \/ N e. NN0 ) )
12	1 2 3 4 5 6 10 8 11	gsummulglem	|- ( ph -> ( G gsum ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsum ( k e. A |-> X ) ) ) )