Theorem zlmodzxzlmod

Description: The ZZ-module ZZ X. ZZ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypothesis	zlmodzxz.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
Assertion	zlmodzxzlmod	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
2		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
3		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
4	1	frlmlmod	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \left\{0,1\right\}\in \mathrm{V}\right)\to Z\in \mathrm{LMod}$$
5	2 3 4	mp2an	$$⊢Z\in \mathrm{LMod}$$
6	1	frlmsca	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \left\{0,1\right\}\in \mathrm{V}\right)\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)$$
7	2 3 6	mp2an	$$⊢{\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)$$
8	5 7	pm3.2i	$$⊢\left(Z\in \mathrm{LMod}\wedge {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(Z\right)\right)$$