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 20704
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 20700 . 2 class ℤMod
2 vg . . 3 setvar 𝑔
3 cvv 3431 . . 3 class V
42cv 1541 . . . . 5 class 𝑔
5 cnx 16892 . . . . . . 7 class ndx
6 csca 16963 . . . . . . 7 class Scalar
75, 6cfv 6432 . . . . . 6 class (Scalar‘ndx)
8 czring 20668 . . . . . 6 class ring
97, 8cop 4573 . . . . 5 class ⟨(Scalar‘ndx), ℤring
10 csts 16862 . . . . 5 class sSet
114, 9, 10co 7271 . . . 4 class (𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩)
12 cvsca 16964 . . . . . 6 class ·𝑠
135, 12cfv 6432 . . . . 5 class ( ·𝑠 ‘ndx)
14 cmg 18698 . . . . . 6 class .g
154, 14cfv 6432 . . . . 5 class (.g𝑔)
1613, 15cop 4573 . . . 4 class ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩
1711, 16, 10co 7271 . . 3 class ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩)
182, 3, 17cmpt 5162 . 2 class (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
191, 18wceq 1542 1 wff ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  zlmval  20715
  Copyright terms: Public domain W3C validator