Definition df-zlm

Description: Augment an abelian group with vector space operations to turn it into a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Assertion	df-zlm	$$⊢\mathrm{\mathbb{Z}Mod}=\left(g\in \mathrm{V}⟼\left(g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czlm	$$class\mathrm{\mathbb{Z}Mod}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarg$$
4		csts	$$class\mathrm{sSet}$$
5		csca	$$class\mathrm{Scalar}$$
6		cnx	$$class\mathrm{ndx}$$
7	6 5	cfv	$$class\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
8		zring	$$class{\mathbb{Z}}_{\mathrm{ring}}$$
9	7 8	cop	$$class⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩$$
10	3 9 4	co	$$class\left(g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)$$
11		cvsca	$$class{\cdot }_{𝑠}$$
12	6 11	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
13		cmg	$$class{\mathrm{\cdot }}_{𝑔}$$
14	3 13	cfv	$$class{\cdot }_g$$
15	12 14	cop	$$class⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩$$
16	10 15 4	co	$$class\left(\left(g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩\right)$$
17	1 2 16	cmpt	$$class\left(g\in \mathrm{V}⟼\left(g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩\right)$$
18	0 17	wceq	$$wff\mathrm{\mathbb{Z}Mod}=\left(g\in \mathrm{V}⟼\left(g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩\right)$$