Theorem zlmodzxz0

Description: The 0 of the ZZ-module ZZ X. ZZ . (Contributed by AV, 20-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	zlmodzxz.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
	zlmodzxz.o	⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
Assertion	zlmodzxz0	⊢ 0 = ( 0g ‘ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		zlmodzxz.o	⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
3		c0ex	⊢ 0 ∈ V
4		1ex	⊢ 1 ∈ V
5		xpprsng	⊢ ( ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ∈ V ) → ( { 0 , 1 } × { 0 } ) = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
6	3 4 3 5	mp3an	⊢ ( { 0 , 1 } × { 0 } ) = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
7		zringring	⊢ ℤring ∈ Ring
8		prex	⊢ { 0 , 1 } ∈ V
9		zring0	⊢ 0 = ( 0g ‘ ℤring )
10	1 9	frlm0	⊢ ( ( ℤring ∈ Ring ∧ { 0 , 1 } ∈ V ) → ( { 0 , 1 } × { 0 } ) = ( 0g ‘ 𝑍 ) )
11	7 8 10	mp2an	⊢ ( { 0 , 1 } × { 0 } ) = ( 0g ‘ 𝑍 )
12	2 6 11	3eqtr2i	⊢ 0 = ( 0g ‘ 𝑍 )