Theorem zlmplusg

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

	Ref	Expression
Hypotheses	zlmbas.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
	zlmplusg.2	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	zlmplusg	$$⊢\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	zlmlem	$$⊢{+}_G={+}_W$$
7	2 6	eqtri	$$⊢\underset{\dot{}}{+}={+}_W$$