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

Metamath Proof Explorer

Theorem zlmval

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
Hypotheses zlmval.w ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
zlmval.m ⊢ · = ( .g ‘ 𝐺 )
Assertion zlmval ( 𝐺 ∈ 𝑉 → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )

Proof

Step Hyp Ref Expression
1 zlmval.w ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2 zlmval.m ⊢ · = ( .g ‘ 𝐺 )
3 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
4 oveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) = ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) )
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( .g ‘ 𝑔 ) = ( .g ‘ 𝐺 ) )
6 5 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( .g ‘ 𝑔 ) = · )
7 6 opeq2d ⊢ ( 𝑔 = 𝐺 → ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ )
8 4 7 oveq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩ ) = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )
9 df-zlm ⊢ ℤMod = ( 𝑔 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝑔 ) ⟩ ) )
10 ovex ⊢ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) ∈ V
11 8 9 10 fvmpt ⊢ ( 𝐺 ∈ V → ( ℤMod ‘ 𝐺 ) = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )
12 3 11 syl ⊢ ( 𝐺 ∈ 𝑉 → ( ℤMod ‘ 𝐺 ) = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )
13 1 12 eqtrid ⊢ ( 𝐺 ∈ 𝑉 → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )