Definition df-zlm 14181

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.)

Assertion

Ref	Expression
df-zlm	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )

Detailed syntax breakdown of Definition df-zlm

Step	Hyp	Ref	Expression
1		czlm 14178	. 2 class ZMod
2		vg	. . 3 setvar g
3		cvv 2763	. . 3 class _V
4	2	cv 1363	. . . . 5 class g
5		cnx 12685	. . . . . . 7 class ndx
6		csca 12768	. . . . . . 7 class Scalar
7	5, 6	cfv 5259	. . . . . 6 class (Scalar ` ndx )
8		czring 14156	. . . . . 6 class ℤring
9	7, 8	cop 3626	. . . . 5 class <. (Scalar ` ndx ) , ℤring >.
10		csts 12686	. . . . 5 class sSet
11	4, 9, 10	co 5923	. . . 4 class ( g sSet <. (Scalar ` ndx ) , ℤring >. )
12		cvsca 12769	. . . . . 6 class .s
13	5, 12	cfv 5259	. . . . 5 class ( .s ` ndx )
14		cmg 13259	. . . . . 6 class .g
15	4, 14	cfv 5259	. . . . 5 class (.g ` g )
16	13, 15	cop 3626	. . . 4 class <. ( .s ` ndx ) , (.g ` g ) >.
17	11, 16, 10	co 5923	. . 3 class ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. )
18	2, 3, 17	cmpt 4095	. 2 class ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
19	1, 18	wceq 1364	1 wff ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )

This definition is referenced by:  zlmval  14193