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 19772
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 19768 . 2 class ℤMod
2 vg . . 3 setvar 𝑔
3 cvv 3186 . . 3 class V
42cv 1479 . . . . 5 class 𝑔
5 cnx 15778 . . . . . . 7 class ndx
6 csca 15865 . . . . . . 7 class Scalar
75, 6cfv 5847 . . . . . 6 class (Scalar‘ndx)
8 zring 19737 . . . . . 6 class ring
97, 8cop 4154 . . . . 5 class ⟨(Scalar‘ndx), ℤring
10 csts 15779 . . . . 5 class sSet
114, 9, 10co 6604 . . . 4 class (𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩)
12 cvsca 15866 . . . . . 6 class ·𝑠
135, 12cfv 5847 . . . . 5 class ( ·𝑠 ‘ndx)
14 cmg 17461 . . . . . 6 class .g
154, 14cfv 5847 . . . . 5 class (.g𝑔)
1613, 15cop 4154 . . . 4 class ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩
1711, 16, 10co 6604 . . 3 class ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩)
182, 3, 17cmpt 4673 . 2 class (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
191, 18wceq 1480 1 wff ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  zlmval  19783
  Copyright terms: Public domain W3C validator