MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-zlm Structured version   Unicode version

Definition df-zlm 17935
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
StepHypRef Expression
1 czlm 17931 . 2  class  ZMod
2 vg . . 3  setvar  g
3 cvv 2971 . . 3  class  _V
42cv 1368 . . . . 5  class  g
5 cnx 14170 . . . . . . 7  class  ndx
6 csca 14240 . . . . . . 7  class Scalar
75, 6cfv 5417 . . . . . 6  class  (Scalar `  ndx )
8 zring 17882 . . . . . 6  classring
97, 8cop 3882 . . . . 5  class  <. (Scalar ` 
ndx ) ,ring >.
10 csts 14171 . . . . 5  class sSet
114, 9, 10co 6090 . . . 4  class  ( g sSet  <. (Scalar `  ndx ) ,ring >. )
12 cvsca 14241 . . . . . 6  class  .s
135, 12cfv 5417 . . . . 5  class  ( .s
`  ndx )
14 cmg 15413 . . . . . 6  class .g
154, 14cfv 5417 . . . . 5  class  (.g `  g
)
1613, 15cop 3882 . . . 4  class  <. ( .s `  ndx ) ,  (.g `  g ) >.
1711, 16, 10co 6090 . . 3  class  ( ( g sSet  <. (Scalar `  ndx ) ,ring >. ) sSet  <. ( .s `  ndx ) ,  (.g `  g ) >.
)
182, 3, 17cmpt 4349 . 2  class  ( g  e.  _V  |->  ( ( g sSet  <. (Scalar `  ndx ) ,ring >. ) sSet  <. ( .s `  ndx ) ,  (.g `  g ) >.
) )
191, 18wceq 1369 1  wff  ZMod  =  ( g  e.  _V  |->  ( ( g sSet  <. (Scalar `  ndx ) ,ring >. ) sSet  <. ( .s `  ndx ) ,  (.g `  g ) >.
) )
Colors of variables: wff setvar class
This definition is referenced by:  zlmval  17946
  Copyright terms: Public domain W3C validator