gsummulc2OLD

Description: Obsolete version of gsummulc2 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 10-Jul-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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

Metamath Proof Explorer

Theorem gsummulc2OLD

Proof