Theorem mnring0gd

Description: The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnring0gd.1	$$⊢F=R\mathrm{MndRing}M$$
	mnring0gd.2	$$⊢A={\mathrm{Base}}_M$$
	mnring0gd.3	$$⊢V=R\mathrm{freeLMod}A$$
	mnring0gd.4	$$⊢\phi \to R\in U$$
	mnring0gd.5	$$⊢\phi \to M\in W$$
Assertion	mnring0gd	$$⊢\phi \to 0_V=0_F$$

Proof

Step	Hyp	Ref	Expression
1		mnring0gd.1	$$⊢F=R\mathrm{MndRing}M$$
2		mnring0gd.2	$$⊢A={\mathrm{Base}}_M$$
3		mnring0gd.3	$$⊢V=R\mathrm{freeLMod}A$$
4		mnring0gd.4	$$⊢\phi \to R\in U$$
5		mnring0gd.5	$$⊢\phi \to M\in W$$
6		eqidd	$$⊢\phi \to {\mathrm{Base}}_V={\mathrm{Base}}_V$$
7		eqid	$$⊢{\mathrm{Base}}_V={\mathrm{Base}}_V$$
8	1 2 3 7 4 5	mnringbased	$$⊢\phi \to {\mathrm{Base}}_V={\mathrm{Base}}_F$$
9	1 2 3 4 5	mnringaddgd	$$⊢\phi \to {+}_V={+}_F$$
10	9	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_V\wedge y\in {\mathrm{Base}}_V\right)\right)\to x{+}_{V}y=x{+}_{F}y$$
11	6 8 10	grpidpropd	$$⊢\phi \to 0_V=0_F$$