Theorem zlm0

Description: Zero of a ZZ -module. (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	zlmlem2.1	|- W = ( ZMod ` G )
	zlm0.1	|- .0. = ( 0g ` G )
Assertion	zlm0	|- .0. = ( 0g ` W )

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	|- W = ( ZMod ` G )
2		zlm0.1	|- .0. = ( 0g ` G )
3		eqid	|- ( Base ` G ) = ( Base ` G )
4	3	a1i	|- ( T. -> ( Base ` G ) = ( Base ` G ) )
5	1 3	zlmbas	|- ( Base ` G ) = ( Base ` W )
6	5	a1i	|- ( T. -> ( Base ` G ) = ( Base ` W ) )
7		eqid	|- ( +g ` G ) = ( +g ` G )
8	1 7	zlmplusg	|- ( +g ` G ) = ( +g ` W )
9	8	a1i	|- ( ( T. /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( +g ` G ) = ( +g ` W ) )
10	9	oveqd	|- ( ( T. /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` W ) y ) )
11	4 6 10	grpidpropd	|- ( T. -> ( 0g ` G ) = ( 0g ` W ) )
12	11	mptru	|- ( 0g ` G ) = ( 0g ` W )
13	2 12	eqtri	|- .0. = ( 0g ` W )