Theorem zlmodzxzlmod

Description: The ZZ-module ZZ X. ZZ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypothesis	zlmodzxz.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
Assertion	zlmodzxzlmod	⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		zringring	⊢ ℤring ∈ Ring
3		prex	⊢ { 0 , 1 } ∈ V
4	1	frlmlmod	⊢ ( ( ℤring ∈ Ring ∧ { 0 , 1 } ∈ V ) → 𝑍 ∈ LMod )
5	2 3 4	mp2an	⊢ 𝑍 ∈ LMod
6	1	frlmsca	⊢ ( ( ℤring ∈ Ring ∧ { 0 , 1 } ∈ V ) → ℤring = ( Scalar ‘ 𝑍 ) )
7	2 3 6	mp2an	⊢ ℤring = ( Scalar ‘ 𝑍 )
8	5 7	pm3.2i	⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )