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

Definition df-zlm 18337
 Description: Augment an abelian group with vector space operations to turn it into a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
Assertion
Ref Expression
df-zlm Mod sSet Scalarring sSet .g

Detailed syntax breakdown of Definition df-zlm
StepHypRef Expression
1 czlm 18333 . 2 Mod
2 vg . . 3
3 cvv 3113 . . 3
42cv 1378 . . . . 5
5 cnx 14487 . . . . . . 7
6 csca 14558 . . . . . . 7 Scalar
75, 6cfv 5588 . . . . . 6 Scalar
8 zring 18284 . . . . . 6 ring
97, 8cop 4033 . . . . 5 Scalarring
10 csts 14488 . . . . 5 sSet
114, 9, 10co 6284 . . . 4 sSet Scalarring
12 cvsca 14559 . . . . . 6
135, 12cfv 5588 . . . . 5
14 cmg 15731 . . . . . 6 .g
154, 14cfv 5588 . . . . 5 .g
1613, 15cop 4033 . . . 4 .g
1711, 16, 10co 6284 . . 3 sSet Scalarring sSet .g
182, 3, 17cmpt 4505 . 2 sSet Scalarring sSet .g
191, 18wceq 1379 1 Mod sSet Scalarring sSet .g
 Colors of variables: wff setvar class This definition is referenced by:  zlmval  18348
 Copyright terms: Public domain W3C validator