Theorem zlm1

Description: Unity element of a ZZ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	zlmlem2.1	|- W = ( ZMod ` G )
	zlm1.1	|- .1. = ( 1r ` G )
Assertion	zlm1	|- .1. = ( 1r ` W )

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	|- W = ( ZMod ` G )
2		zlm1.1	|- .1. = ( 1r ` 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	|- ( .r ` G ) = ( .r ` G )
8	1 7	zlmmulr	|- ( .r ` G ) = ( .r ` W )
9	8	a1i	|- ( ( T. /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( .r ` G ) = ( .r ` W ) )
10	9	oveqd	|- ( ( T. /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( .r ` G ) y ) = ( x ( .r ` W ) y ) )
11	4 6 10	rngidpropd	|- ( T. -> ( 1r ` G ) = ( 1r ` W ) )
12	11	mptru	|- ( 1r ` G ) = ( 1r ` W )
13	2 12	eqtri	|- .1. = ( 1r ` W )