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	|- ZMod = ( g e. _V |-> ( ( g sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` g ) >. ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czlm	|- ZMod
1		vg	|- g
2		cvv	|- _V
3	1	cv	|- g
4		csts	|- sSet
5		csca	|- Scalar
6		cnx	|- ndx
7	6 5	cfv	|- ( Scalar ` ndx )
8		zring	|- ZZring
9	7 8	cop	|- <. ( Scalar ` ndx ) , ZZring >.
10	3 9 4	co	|- ( g sSet <. ( Scalar ` ndx ) , ZZring >. )
11		cvsca	|- .s
12	6 11	cfv	|- ( .s ` ndx )
13		cmg	|- .g
14	3 13	cfv	|- ( .g ` g )
15	12 14	cop	|- <. ( .s ` ndx ) , ( .g ` g ) >.
16	10 15 4	co	|- ( ( g sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` g ) >. )
17	1 2 16	cmpt	|- ( g e. _V |-> ( ( g sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` g ) >. ) )
18	0 17	wceq	|- ZMod = ( g e. _V |-> ( ( g sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` g ) >. ) )