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

Definition df-zlm 16456
Description: Augment an abelian group with vector space operations to turn it into a  ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
df-zlm  |-  ZMod  =  ( g  e.  _V  |->  ( ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ )
>. ) sSet  <. ( .s
`  ndx ) ,  (.g `  g ) >. )
)

Detailed syntax breakdown of Definition df-zlm
StepHypRef Expression
1 czlm 16452 . 2  class  ZMod
2 vg . . 3  set  g
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . . 5  class  g
5 cnx 13145 . . . . . . 7  class  ndx
6 csca 13211 . . . . . . 7  class Scalar
75, 6cfv 5255 . . . . . 6  class  (Scalar `  ndx )
8 ccnfld 16377 . . . . . . 7  classfld
9 cz 10024 . . . . . . 7  class  ZZ
10 cress 13149 . . . . . . 7  classs
118, 9, 10co 5858 . . . . . 6  class  (flds  ZZ )
127, 11cop 3643 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (flds  ZZ )
>.
13 csts 13146 . . . . 5  class sSet
144, 12, 13co 5858 . . . 4  class  ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ ) >. )
15 cvsca 13212 . . . . . 6  class  .s
165, 15cfv 5255 . . . . 5  class  ( .s
`  ndx )
17 cmg 14366 . . . . . 6  class .g
184, 17cfv 5255 . . . . 5  class  (.g `  g
)
1916, 18cop 3643 . . . 4  class  <. ( .s `  ndx ) ,  (.g `  g ) >.
2014, 19, 13co 5858 . . 3  class  ( ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ ) >. ) sSet  <.
( .s `  ndx ) ,  (.g `  g
) >. )
212, 3, 20cmpt 4077 . 2  class  ( g  e.  _V  |->  ( ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ ) >. ) sSet  <.
( .s `  ndx ) ,  (.g `  g
) >. ) )
221, 21wceq 1623 1  wff  ZMod  =  ( g  e.  _V  |->  ( ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ )
>. ) sSet  <. ( .s
`  ndx ) ,  (.g `  g ) >. )
)
Colors of variables: wff set class
This definition is referenced by:  zlmval  16470
  Copyright terms: Public domain W3C validator