Theorem zlm0

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

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

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		zlm0.1	$$⊢\underset{\dot{}}{0}=0_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	$$⊢{+}_G={+}_G$$
8	1 7	zlmplusg	$$⊢{+}_G={+}_W$$
9	8	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to {+}_G={+}_W$$
10	9	oveqd	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y=x{+}_{W}y$$
11	4 6 10	grpidpropd	$$⊢\top \to 0_G=0_W$$
12	11	mptru	$$⊢0_G=0_W$$
13	2 12	eqtri	$$⊢\underset{\dot{}}{0}=0_W$$