Theorem zlmmulr

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

	Ref	Expression
Hypotheses	zlmbas.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
	zlmmulr.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	zlmmulr	$$⊢\underset{\dot{}}{·}={\cdot }_W$$

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		zlmmulr.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		df-mulr	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}3$$
4		3nn	$$⊢3\in \mathbb{N}$$
5		3lt5	$$⊢3<5$$
6	1 3 4 5	zlmlem	$$⊢{\cdot }_G={\cdot }_W$$
7	2 6	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_W$$