Theorem mnringlmodd

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

	Ref	Expression
Hypotheses	mnringlmodd.1	|- F = ( R MndRing M )
	mnringlmodd.2	|- ( ph -> R e. Ring )
	mnringlmodd.3	|- ( ph -> M e. U )
Assertion	mnringlmodd	|- ( ph -> F e. LMod )

Proof

Step	Hyp	Ref	Expression
1		mnringlmodd.1	|- F = ( R MndRing M )
2		mnringlmodd.2	|- ( ph -> R e. Ring )
3		mnringlmodd.3	|- ( ph -> M e. U )
4		fvexd	|- ( ph -> ( Base ` M ) e. _V )
5		eqid	|- ( R freeLMod ( Base ` M ) ) = ( R freeLMod ( Base ` M ) )
6	5	frlmlmod	|- ( ( R e. Ring /\ ( Base ` M ) e. _V ) -> ( R freeLMod ( Base ` M ) ) e. LMod )
7	2 4 6	syl2anc	|- ( ph -> ( R freeLMod ( Base ` M ) ) e. LMod )
8		eqidd	|- ( ph -> ( Base ` ( R freeLMod ( Base ` M ) ) ) = ( Base ` ( R freeLMod ( Base ` M ) ) ) )
9		eqid	|- ( Base ` M ) = ( Base ` M )
10		eqid	|- ( Base ` ( R freeLMod ( Base ` M ) ) ) = ( Base ` ( R freeLMod ( Base ` M ) ) )
11	1 9 5 10 2 3	mnringbased	|- ( ph -> ( Base ` ( R freeLMod ( Base ` M ) ) ) = ( Base ` F ) )
12	1 9 5 2 3	mnringaddgd	|- ( ph -> ( +g ` ( R freeLMod ( Base ` M ) ) ) = ( +g ` F ) )
13	12	oveqdr	|- ( ( ph /\ ( x e. ( Base ` ( R freeLMod ( Base ` M ) ) ) /\ y e. ( Base ` ( R freeLMod ( Base ` M ) ) ) ) ) -> ( x ( +g ` ( R freeLMod ( Base ` M ) ) ) y ) = ( x ( +g ` F ) y ) )
14	5	frlmsca	|- ( ( R e. Ring /\ ( Base ` M ) e. _V ) -> R = ( Scalar ` ( R freeLMod ( Base ` M ) ) ) )
15	2 4 14	syl2anc	|- ( ph -> R = ( Scalar ` ( R freeLMod ( Base ` M ) ) ) )
16	1 2 3	mnringscad	|- ( ph -> R = ( Scalar ` F ) )
17		eqid	|- ( Base ` R ) = ( Base ` R )
18	1 9 5 2 3	mnringvscad	|- ( ph -> ( .s ` ( R freeLMod ( Base ` M ) ) ) = ( .s ` F ) )
19	18	oveqdr	|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` ( R freeLMod ( Base ` M ) ) ) ) ) -> ( x ( .s ` ( R freeLMod ( Base ` M ) ) ) y ) = ( x ( .s ` F ) y ) )
20	8 11 13 15 16 17 19	lmodpropd	|- ( ph -> ( ( R freeLMod ( Base ` M ) ) e. LMod <-> F e. LMod ) )
21	7 20	mpbid	|- ( ph -> F e. LMod )