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 20628
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 20624 . 2 class ℤMod
2 vg . . 3 setvar 𝑔
3 cvv 3473 . . 3 class V
42cv 1536 . . . . 5 class 𝑔
5 cnx 16459 . . . . . . 7 class ndx
6 csca 16547 . . . . . . 7 class Scalar
75, 6cfv 6331 . . . . . 6 class (Scalar‘ndx)
8 zring 20593 . . . . . 6 class ring
97, 8cop 4549 . . . . 5 class ⟨(Scalar‘ndx), ℤring
10 csts 16460 . . . . 5 class sSet
114, 9, 10co 7133 . . . 4 class (𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩)
12 cvsca 16548 . . . . . 6 class ·𝑠
135, 12cfv 6331 . . . . 5 class ( ·𝑠 ‘ndx)
14 cmg 18203 . . . . . 6 class .g
154, 14cfv 6331 . . . . 5 class (.g𝑔)
1613, 15cop 4549 . . . 4 class ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩
1711, 16, 10co 7133 . . 3 class ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩)
182, 3, 17cmpt 5122 . 2 class (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
191, 18wceq 1537 1 wff ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  zlmval  20639
  Copyright terms: Public domain W3C validator