Theorem zlmmulr

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

	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		df-mulr	|- .r = Slot 3
4		3nn	|- 3 e. NN
5		3lt5	|- 3 < 5
6	1 3 4 5	zlmlem	|- ( .r ` G ) = ( .r ` W )
7	2 6	eqtri	|- .x. = ( .r ` W )