Theorem gsummulc2

Description: A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019) Remove unused hypothesis. (Revised by SN, 7-Mar-2025)

	Ref	Expression
Hypotheses	gsummulc1.b	|- B = ( Base ` R )
	gsummulc1.z	|- .0. = ( 0g ` R )
	gsummulc1.t	|- .x. = ( .r ` R )
	gsummulc1.r	|- ( ph -> R e. Ring )
	gsummulc1.a	|- ( ph -> A e. V )
	gsummulc1.y	|- ( ph -> Y e. B )
	gsummulc1.x	|- ( ( ph /\ k e. A ) -> X e. B )
	gsummulc1.n	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
Assertion	gsummulc2	|- ( ph -> ( R gsum ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummulc1.b	|- B = ( Base ` R )
2		gsummulc1.z	|- .0. = ( 0g ` R )
3		gsummulc1.t	|- .x. = ( .r ` R )
4		gsummulc1.r	|- ( ph -> R e. Ring )
5		gsummulc1.a	|- ( ph -> A e. V )
6		gsummulc1.y	|- ( ph -> Y e. B )
7		gsummulc1.x	|- ( ( ph /\ k e. A ) -> X e. B )
8		gsummulc1.n	|- ( ph -> ( k e. A |-> X ) finSupp .0. )
9	4	ringcmnd	|- ( ph -> R e. CMnd )
10		ringmnd	|- ( R e. Ring -> R e. Mnd )
11	4 10	syl	|- ( ph -> R e. Mnd )
12	1 3	ringlghm	|- ( ( R e. Ring /\ Y e. B ) -> ( x e. B |-> ( Y .x. x ) ) e. ( R GrpHom R ) )
13	4 6 12	syl2anc	|- ( ph -> ( x e. B |-> ( Y .x. x ) ) e. ( R GrpHom R ) )
14		ghmmhm	|- ( ( x e. B |-> ( Y .x. x ) ) e. ( R GrpHom R ) -> ( x e. B |-> ( Y .x. x ) ) e. ( R MndHom R ) )
15	13 14	syl	|- ( ph -> ( x e. B |-> ( Y .x. x ) ) e. ( R MndHom R ) )
16		oveq2	|- ( x = X -> ( Y .x. x ) = ( Y .x. X ) )
17		oveq2	|- ( x = ( R gsum ( k e. A |-> X ) ) -> ( Y .x. x ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) )
18	1 2 9 11 5 15 7 8 16 17	gsummhm2	|- ( ph -> ( R gsum ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsum ( k e. A |-> X ) ) ) )