Theorem mnring0g2d

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

	Ref	Expression
Hypotheses	mnring0g2d.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnring0g2d.2	$$⊢\underset{\dot{}}{0}=0_R$$
	mnring0g2d.3	$$⊢A={\mathrm{Base}}_M$$
	mnring0g2d.4	$$⊢\phi \to R\in \mathrm{Ring}$$
	mnring0g2d.5	$$⊢\phi \to M\in W$$
Assertion	mnring0g2d	$$⊢\phi \to A\times \left\{\underset{\dot{}}{0}\right\}=0_F$$

Proof

Step	Hyp	Ref	Expression
1		mnring0g2d.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnring0g2d.2	$$⊢\underset{\dot{}}{0}=0_R$$
3		mnring0g2d.3	$$⊢A={\mathrm{Base}}_M$$
4		mnring0g2d.4	$$⊢\phi \to R\in \mathrm{Ring}$$
5		mnring0g2d.5	$$⊢\phi \to M\in W$$
6	3	fvexi	$$⊢A\in \mathrm{V}$$
7		eqid	$$⊢R\mathrm{freeLMod}A=R\mathrm{freeLMod}A$$
8	7 2	frlm0	$$⊢\left(R\in \mathrm{Ring}\wedge A\in \mathrm{V}\right)\to A\times \left\{\underset{\dot{}}{0}\right\}=0_{\left(R\mathrm{freeLMod}A\right)}$$
9	4 6 8	sylancl	$$⊢\phi \to A\times \left\{\underset{\dot{}}{0}\right\}=0_{\left(R\mathrm{freeLMod}A\right)}$$
10	1 3 7 4 5	mnring0gd	$$⊢\phi \to 0_{\left(R\mathrm{freeLMod}A\right)}=0_F$$
11	9 10	eqtrd	$$⊢\phi \to A\times \left\{\underset{\dot{}}{0}\right\}=0_F$$