Theorem zlm1

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

	Ref	Expression
Hypotheses	zlmlem2.1	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
	zlm1.1	$$⊢\underset{\dot{}}{1}=1_G$$
Assertion	zlm1	$$⊢\underset{\dot{}}{1}=1_W$$

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		zlm1.1	$$⊢\underset{\dot{}}{1}=1_G$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4	3	a1i	$$⊢\top \to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	1 3	zlmbas	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_W$$
6	5	a1i	$$⊢\top \to {\mathrm{Base}}_G={\mathrm{Base}}_W$$
7		eqid	$$⊢{\cdot }_G={\cdot }_G$$
8	1 7	zlmmulr	$$⊢{\cdot }_G={\cdot }_W$$
9	8	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to {\cdot }_G={\cdot }_W$$
10	9	oveqd	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{\cdot }_{G}y=x{\cdot }_{W}y$$
11	4 6 10	rngidpropd	$$⊢\top \to 1_G=1_W$$
12	11	mptru	$$⊢1_G=1_W$$
13	2 12	eqtri	$$⊢\underset{\dot{}}{1}=1_W$$