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

Definition df-zlm 16472
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 16468 . 2  class  ZMod
2 vg . . 3  set  g
3 cvv 2801 . . 3  class  _V
42cv 1631 . . . . 5  class  g
5 cnx 13161 . . . . . . 7  class  ndx
6 csca 13227 . . . . . . 7  class Scalar
75, 6cfv 5271 . . . . . 6  class  (Scalar `  ndx )
8 ccnfld 16393 . . . . . . 7  classfld
9 cz 10040 . . . . . . 7  class  ZZ
10 cress 13165 . . . . . . 7  classs
118, 9, 10co 5874 . . . . . 6  class  (flds  ZZ )
127, 11cop 3656 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (flds  ZZ )
>.
13 csts 13162 . . . . 5  class sSet
144, 12, 13co 5874 . . . 4  class  ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ ) >. )
15 cvsca 13228 . . . . . 6  class  .s
165, 15cfv 5271 . . . . 5  class  ( .s
`  ndx )
17 cmg 14382 . . . . . 6  class .g
184, 17cfv 5271 . . . . 5  class  (.g `  g
)
1916, 18cop 3656 . . . 4  class  <. ( .s `  ndx ) ,  (.g `  g ) >.
2014, 19, 13co 5874 . . 3  class  ( ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ ) >. ) sSet  <.
( .s `  ndx ) ,  (.g `  g
) >. )
212, 3, 20cmpt 4093 . 2  class  ( g  e.  _V  |->  ( ( g sSet  <. (Scalar `  ndx ) ,  (flds  ZZ ) >. ) sSet  <.
( .s `  ndx ) ,  (.g `  g
) >. ) )
221, 21wceq 1632 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  16486
  Copyright terms: Public domain W3C validator