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 = ( 𝑔 ∈ 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 ‘ 𝑔 ) ⟩ ) )