This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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