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 21053
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 21049 . 2 class ℤMod
2 vg . . 3 setvar 𝑔
3 cvv 3474 . . 3 class V
42cv 1540 . . . . 5 class 𝑔
5 cnx 17125 . . . . . . 7 class ndx
6 csca 17199 . . . . . . 7 class Scalar
75, 6cfv 6543 . . . . . 6 class (Scalar‘ndx)
8 czring 21016 . . . . . 6 class ring
97, 8cop 4634 . . . . 5 class ⟨(Scalar‘ndx), ℤring
10 csts 17095 . . . . 5 class sSet
114, 9, 10co 7408 . . . 4 class (𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩)
12 cvsca 17200 . . . . . 6 class ·𝑠
135, 12cfv 6543 . . . . 5 class ( ·𝑠 ‘ndx)
14 cmg 18949 . . . . . 6 class .g
154, 14cfv 6543 . . . . 5 class (.g𝑔)
1613, 15cop 4634 . . . 4 class ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩
1711, 16, 10co 7408 . . 3 class ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩)
182, 3, 17cmpt 5231 . 2 class (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
191, 18wceq 1541 1 wff ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  zlmval  21064
  Copyright terms: Public domain W3C validator