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	|- Z = ( ZZring freeLMod { 0 , 1 } )
	zlmodzxz.o	|- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
Assertion	zlmodzxz0	|- .0. = ( 0g ` Z )

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	|- Z = ( ZZring freeLMod { 0 , 1 } )
2		zlmodzxz.o	|- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
3		c0ex	|- 0 e. _V
4		1ex	|- 1 e. _V
5		xpprsng	|- ( ( 0 e. _V /\ 1 e. _V /\ 0 e. _V ) -> ( { 0 , 1 } X. { 0 } ) = { <. 0 , 0 >. , <. 1 , 0 >. } )
6	3 4 3 5	mp3an	|- ( { 0 , 1 } X. { 0 } ) = { <. 0 , 0 >. , <. 1 , 0 >. }
7		zringring	|- ZZring e. Ring
8		prex	|- { 0 , 1 } e. _V
9		zring0	|- 0 = ( 0g ` ZZring )
10	1 9	frlm0	|- ( ( ZZring e. Ring /\ { 0 , 1 } e. _V ) -> ( { 0 , 1 } X. { 0 } ) = ( 0g ` Z ) )
11	7 8 10	mp2an	|- ( { 0 , 1 } X. { 0 } ) = ( 0g ` Z )
12	2 6 11	3eqtr2i	|- .0. = ( 0g ` Z )