Theorem mnringlmodd

Description: Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringlmodd.1	$$⊢F=R\mathrm{MndRing}M$$
	mnringlmodd.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	mnringlmodd.3	$$⊢\phi \to M\in U$$
Assertion	mnringlmodd	$$⊢\phi \to F\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		mnringlmodd.1	$$⊢F=R\mathrm{MndRing}M$$
2		mnringlmodd.2	$$⊢\phi \to R\in \mathrm{Ring}$$
3		mnringlmodd.3	$$⊢\phi \to M\in U$$
4		fvexd	$$⊢\phi \to {\mathrm{Base}}_M\in \mathrm{V}$$
5		eqid	$$⊢R\mathrm{freeLMod}{\mathrm{Base}}_M=R\mathrm{freeLMod}{\mathrm{Base}}_M$$
6	5	frlmlmod	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{Base}}_M\in \mathrm{V}\right)\to R\mathrm{freeLMod}{\mathrm{Base}}_M\in \mathrm{LMod}$$
7	2 4 6	syl2anc	$$⊢\phi \to R\mathrm{freeLMod}{\mathrm{Base}}_M\in \mathrm{LMod}$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}={\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}$$
9		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
10		eqid	$$⊢{\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}={\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}$$
11	1 9 5 10 2 3	mnringbased	$$⊢\phi \to {\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}={\mathrm{Base}}_F$$
12	1 9 5 2 3	mnringaddgd	$$⊢\phi \to {+}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}={+}_F$$
13	12	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}\wedge y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}\right)\right)\to x{+}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}y=x{+}_{F}y$$
14	5	frlmsca	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{Base}}_M\in \mathrm{V}\right)\to R=\mathrm{Scalar}\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)$$
15	2 4 14	syl2anc	$$⊢\phi \to R=\mathrm{Scalar}\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)$$
16	1 2 3	mnringscad	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$
17		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
18	1 9 5 2 3	mnringvscad	$$⊢\phi \to {\cdot }_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}={\cdot }_F$$
19	18	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}\right)\right)\to x{\cdot }_{\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)}y=x{\cdot }_{F}y$$
20	8 11 13 15 16 17 19	lmodpropd	$$⊢\phi \to \left(R\mathrm{freeLMod}{\mathrm{Base}}_M\in \mathrm{LMod}\leftrightarrow F\in \mathrm{LMod}\right)$$
21	7 20	mpbid	$$⊢\phi \to F\in \mathrm{LMod}$$