Theorem zlmclm

Description: The ZZ -module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015)

	Ref	Expression
Hypothesis	zlmclm.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
Assertion	zlmclm	$$⊢G\in \mathrm{Abel}\leftrightarrow W\in \mathrm{CMod}$$

Proof

Step	Hyp	Ref	Expression
1		zlmclm.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2	1	zlmlmod	$$⊢G\in \mathrm{Abel}\leftrightarrow W\in \mathrm{LMod}$$
3	2	biimpi	$$⊢G\in \mathrm{Abel}\to W\in \mathrm{LMod}$$
4	1	zlmsca	$$⊢G\in \mathrm{Abel}\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(W\right)$$
5		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
6	4 5	eqtr3di	$$⊢G\in \mathrm{Abel}\to \mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
7		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
8	7	a1i	$$⊢G\in \mathrm{Abel}\to \mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
9		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
10	9	isclmi	$$⊢\left(W\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\wedge \mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to W\in \mathrm{CMod}$$
11	3 6 8 10	syl3anc	$$⊢G\in \mathrm{Abel}\to W\in \mathrm{CMod}$$
12		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
13	12 2	sylibr	$$⊢W\in \mathrm{CMod}\to G\in \mathrm{Abel}$$
14	11 13	impbii	$$⊢G\in \mathrm{Abel}\leftrightarrow W\in \mathrm{CMod}$$