This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-zlm

Description: Augment an abelian group with vector space operations to turn it into a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Assertion df-zlm ⊢ ℤMod = g ∈ V ⟼ g sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ g

Detailed syntax breakdown

Step Hyp Ref Expression
0 czlm class ℤMod
1 vg setvar g
2 cvv class V
3 1 cv setvar g
4 csts class sSet
5 csca class Scalar
6 cnx class ndx
7 6 5 cfv class Scalar ⁡ ndx
8 czring class ℤ ring
9 7 8 cop class Scalar ⁡ ndx ℤ ring
10 3 9 4 co class g sSet Scalar ⁡ ndx ℤ ring
11 cvsca class ⋅ 𝑠
12 6 11 cfv class ⋅ ndx
13 cmg class ⋅ 𝑔
14 3 13 cfv class ⋅ g
15 12 14 cop class ⋅ ndx ⋅ g
16 10 15 4 co class g sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ g
17 1 2 16 cmpt class g ∈ V ⟼ g sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ g
18 0 17 wceq wff ℤMod = g ∈ V ⟼ g sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ g