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	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
	zlmmulr.2	⊢ · = ( .r ‘ 𝐺 )
Assertion	zlmmulr	⊢ · = ( .r ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2		zlmmulr.2	⊢ · = ( .r ‘ 𝐺 )
3		mulrid	⊢ .r = Slot ( .r ‘ ndx )
4		scandxnmulrndx	⊢ ( Scalar ‘ ndx ) ≠ ( .r ‘ ndx )
5	4	necomi	⊢ ( .r ‘ ndx ) ≠ ( Scalar ‘ ndx )
6		vscandxnmulrndx	⊢ ( ·𝑠 ‘ ndx ) ≠ ( .r ‘ ndx )
7	6	necomi	⊢ ( .r ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
8	1 3 5 7	zlmlem	⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝑊 )
9	2 8	eqtri	⊢ · = ( .r ‘ 𝑊 )