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

Definition df-zlm 16783
 Description: Augment an abelian group with vector space operations to turn it into a -module. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
df-zlm Mod sSet Scalar flds sSet .g

Detailed syntax breakdown of Definition df-zlm
StepHypRef Expression
1 czlm 16779 . 2 Mod
2 vg . . 3
3 cvv 2956 . . 3
42cv 1651 . . . . 5
5 cnx 13466 . . . . . . 7
6 csca 13532 . . . . . . 7 Scalar
75, 6cfv 5454 . . . . . 6 Scalar
8 ccnfld 16703 . . . . . . 7 fld
9 cz 10282 . . . . . . 7
10 cress 13470 . . . . . . 7 s
118, 9, 10co 6081 . . . . . 6 flds
127, 11cop 3817 . . . . 5 Scalar flds
13 csts 13467 . . . . 5 sSet
144, 12, 13co 6081 . . . 4 sSet Scalar flds
15 cvsca 13533 . . . . . 6
165, 15cfv 5454 . . . . 5
17 cmg 14689 . . . . . 6 .g
184, 17cfv 5454 . . . . 5 .g
1916, 18cop 3817 . . . 4 .g
2014, 19, 13co 6081 . . 3 sSet Scalar flds sSet .g
212, 3, 20cmpt 4266 . 2 sSet Scalar flds sSet .g
221, 21wceq 1652 1 Mod sSet Scalar flds sSet .g
 Colors of variables: wff set class This definition is referenced by:  zlmval  16797
 Copyright terms: Public domain W3C validator