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	syl5eq	⊢ ( 𝐺 ∈ 𝑉 → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )