Theorem zlmmulr

Description: Ring operation of a ZZ -module (if present). (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)

	Ref	Expression
Hypotheses	zlmbas.w	|- W = ( ZMod ` G )
	zlmmulr.2	|- .x. = ( .r ` G )
Assertion	zlmmulr	|- .x. = ( .r ` W )

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	|- W = ( ZMod ` G )
2		zlmmulr.2	|- .x. = ( .r ` G )
3		mulrid	|- .r = Slot ( .r ` ndx )
4		scandxnmulrndx	|- ( Scalar ` ndx ) =/= ( .r ` ndx )
5	4	necomi	|- ( .r ` ndx ) =/= ( Scalar ` ndx )
6		vscandxnmulrndx	|- ( .s ` ndx ) =/= ( .r ` ndx )
7	6	necomi	|- ( .r ` ndx ) =/= ( .s ` ndx )
8	1 3 5 7	zlmlem	|- ( .r ` G ) = ( .r ` W )
9	2 8	eqtri	|- .x. = ( .r ` W )