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 = ( 𝑔 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czlm	⊢ ℤMod
1		vg	⊢ 𝑔
2		cvv	⊢ V
3	1	cv	⊢ 𝑔
4		csts	⊢ sSet
5		csca	⊢ Scalar
6		cnx	⊢ ndx
7	6 5	cfv	⊢ ( Scalar ‘ ndx )
8		czring	⊢ ℤring
9	7 8	cop	⊢ ⟨ ( Scalar ‘ ndx ) , ℤring ⟩
10	3 9 4	co	⊢ ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ )
11		cvsca	⊢ ·𝑠
12	6 11	cfv	⊢ ( ·𝑠 ‘ ndx )
13		cmg	⊢ .g
14	3 13	cfv	⊢ ( .g ‘ 𝑔 )
15	12 14	cop	⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩
16	10 15 4	co	⊢ ( ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩ )
17	1 2 16	cmpt	⊢ ( 𝑔 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩ ) )
18	0 17	wceq	⊢ ℤMod = ( 𝑔 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩ ) )