Theorem gsummulglem

Description: Lemma for gsummulg and gsummulgz . (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. )
	gsummulglem.g	|- ( ph -> G e. CMnd )
	gsummulglem.n	|- ( ph -> N e. ZZ )
	gsummulglem.o	|- ( ph -> ( G e. Abel \/ N e. NN0 ) )
Assertion	gsummulglem	|- ( 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		gsummulglem.g	|- ( ph -> G e. CMnd )
8		gsummulglem.n	|- ( ph -> N e. ZZ )
9		gsummulglem.o	|- ( ph -> ( G e. Abel \/ N e. NN0 ) )
10		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
11	7 10	syl	|- ( ph -> G e. Mnd )
12	1 3	mulgghm	|- ( ( G e. Abel /\ N e. ZZ ) -> ( x e. B |-> ( N .x. x ) ) e. ( G GrpHom G ) )
13		ghmmhm	|- ( ( x e. B |-> ( N .x. x ) ) e. ( G GrpHom G ) -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) )
14	12 13	syl	|- ( ( G e. Abel /\ N e. ZZ ) -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) )
15	14	expcom	|- ( N e. ZZ -> ( G e. Abel -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) ) )
16	8 15	syl	|- ( ph -> ( G e. Abel -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) ) )
17	1 3	mulgmhm	|- ( ( G e. CMnd /\ N e. NN0 ) -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) )
18	17	ex	|- ( G e. CMnd -> ( N e. NN0 -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) ) )
19	7 18	syl	|- ( ph -> ( N e. NN0 -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) ) )
20	16 19 9	mpjaod	|- ( ph -> ( x e. B |-> ( N .x. x ) ) e. ( G MndHom G ) )
21		oveq2	|- ( x = X -> ( N .x. x ) = ( N .x. X ) )
22		oveq2	|- ( x = ( G gsum ( k e. A |-> X ) ) -> ( N .x. x ) = ( N .x. ( G gsum ( k e. A |-> X ) ) ) )
23	1 2 7 11 4 20 5 6 21 22	gsummhm2	|- ( ph -> ( G gsum ( k e. A |-> ( N .x. X ) ) ) = ( N .x. ( G gsum ( k e. A |-> X ) ) ) )