mnringlmodd

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

	Ref	Expression
Hypotheses	mnringlmodd.1	No typesetting found for \|- F = ( R MndRing M ) with typecode \|-
	mnringlmodd.2	$⊢ φ \to R \in Ring$
	mnringlmodd.3	$⊢ φ \to M \in U$
Assertion	mnringlmodd	$⊢ φ \to F \in LMod$

Proof

Step	Hyp	Ref	Expression
1		mnringlmodd.1	Could not format F = ( R MndRing M ) : No typesetting found for \|- F = ( R MndRing M ) with typecode \|-
2		mnringlmodd.2	$⊢ φ \to R \in Ring$
3		mnringlmodd.3	$⊢ φ \to M \in U$
4		fvexd	$⊢ φ \to {Base}_{M} \in V$
5		eqid	$⊢ R freeLMod {Base}_{M} = R freeLMod {Base}_{M}$
6	5	frlmlmod	$⊢ (R \in Ring \land {Base}_{M} \in V) \to R freeLMod {Base}_{M} \in LMod$
7	2 4 6	syl2anc	$⊢ φ \to R freeLMod {Base}_{M} \in LMod$
8		eqidd	$⊢ φ \to {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	$⊢ φ \to {Base}_{(R freeLMod {Base}_{M})} = {Base}_{F}$
12	1 9 5 2 3	mnringaddgd	$⊢ φ \to +_{(R freeLMod {Base}_{M})} = +_{F}$
13	12	oveqdr	$⊢ (φ \land (x \in {Base}_{(R freeLMod {Base}_{M})} \land y \in {Base}_{(R freeLMod {Base}_{M})})) \to x +_{(R freeLMod {Base}_{M})} y = x +_{F} y$
14	5	frlmsca	$⊢ (R \in Ring \land {Base}_{M} \in V) \to R = Scalar (R freeLMod {Base}_{M})$
15	2 4 14	syl2anc	$⊢ φ \to R = Scalar (R freeLMod {Base}_{M})$
16	1 2 3	mnringscad	$⊢ φ \to R = Scalar (F)$
17		eqid	$⊢ {Base}_{R} = {Base}_{R}$
18	1 9 5 2 3	mnringvscad	$⊢ φ \to \cdot_{(R freeLMod {Base}_{M})} = \cdot_{F}$
19	18	oveqdr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{(R freeLMod {Base}_{M})})) \to x \cdot_{(R freeLMod {Base}_{M})} y = x \cdot_{F} y$
20	8 11 13 15 16 17 19	lmodpropd	$⊢ φ \to (R freeLMod {Base}_{M} \in LMod \leftrightarrow F \in LMod)$
21	7 20	mpbid	$⊢ φ \to F \in LMod$

Metamath Proof Explorer

Theorem mnringlmodd

Proof