Theorem zlmplusgOLD

Description: Obsolete version of zlmbas as of 3-Nov-2024. Group operation of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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