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

Definition df-zlm 20075
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 = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))

Detailed syntax breakdown of Definition df-zlm
StepHypRef Expression
1 czlm 20071 . 2 class ℤMod
2 vg . . 3 setvar 𝑔
3 cvv 3340 . . 3 class V
42cv 1631 . . . . 5 class 𝑔
5 cnx 16076 . . . . . . 7 class ndx
6 csca 16166 . . . . . . 7 class Scalar
75, 6cfv 6049 . . . . . 6 class (Scalar‘ndx)
8 zring 20040 . . . . . 6 class ring
97, 8cop 4327 . . . . 5 class ⟨(Scalar‘ndx), ℤring
10 csts 16077 . . . . 5 class sSet
114, 9, 10co 6814 . . . 4 class (𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩)
12 cvsca 16167 . . . . . 6 class ·𝑠
135, 12cfv 6049 . . . . 5 class ( ·𝑠 ‘ndx)
14 cmg 17761 . . . . . 6 class .g
154, 14cfv 6049 . . . . 5 class (.g𝑔)
1613, 15cop 4327 . . . 4 class ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩
1711, 16, 10co 6814 . . 3 class ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩)
182, 3, 17cmpt 4881 . 2 class (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
191, 18wceq 1632 1 wff ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  zlmval  20086
  Copyright terms: Public domain W3C validator