Definition df-zlm 21515

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

Step	Hyp	Ref	Expression
1		czlm 21511	. 2 class ℤMod
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4	2	cv 1539	. . . . 5 class 𝑔
5		cnx 17230	. . . . . . 7 class ndx
6		csca 17300	. . . . . . 7 class Scalar
7	5, 6	cfv 6561	. . . . . 6 class (Scalar‘ndx)
8		czring 21457	. . . . . 6 class ℤring
9	7, 8	cop 4632	. . . . 5 class ⟨(Scalar‘ndx), ℤring⟩
10		csts 17200	. . . . 5 class sSet
11	4, 9, 10	co 7431	. . . 4 class (𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩)
12		cvsca 17301	. . . . . 6 class ·𝑠
13	5, 12	cfv 6561	. . . . 5 class ( ·𝑠 ‘ndx)
14		cmg 19085	. . . . . 6 class .g
15	4, 14	cfv 6561	. . . . 5 class (.g‘𝑔)
16	13, 15	cop 4632	. . . 4 class ⟨( ·𝑠 ‘ndx), (.g‘𝑔)⟩
17	11, 16, 10	co 7431	. . 3 class ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝑔)⟩)
18	2, 3, 17	cmpt 5225	. 2 class (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝑔)⟩))
19	1, 18	wceq 1540	1 wff ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝑔)⟩))

This definition is referenced by:  zlmval  21526