Theorem mnringlmodd

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

	Ref	Expression
Hypotheses	mnringlmodd.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringlmodd.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mnringlmodd.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
Assertion	mnringlmodd	⊢ ( 𝜑 → 𝐹 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		mnringlmodd.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringlmodd.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		mnringlmodd.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
4		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑀 ) ∈ V )
5		eqid	⊢ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) = ( 𝑅 freeLMod ( Base ‘ 𝑀 ) )
6	5	frlmlmod	⊢ ( ( 𝑅 ∈ Ring ∧ ( Base ‘ 𝑀 ) ∈ V ) → ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ∈ LMod )
7	2 4 6	syl2anc	⊢ ( 𝜑 → ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ∈ LMod )
8		eqidd	⊢ ( 𝜑 → ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) )
9		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
10		eqid	⊢ ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) )
11	1 9 5 10 2 3	mnringbased	⊢ ( 𝜑 → ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) = ( Base ‘ 𝐹 ) )
12	1 9 5 2 3	mnringaddgd	⊢ ( 𝜑 → ( +g ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) = ( +g ‘ 𝐹 ) )
13	12	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) )
14	5	frlmsca	⊢ ( ( 𝑅 ∈ Ring ∧ ( Base ‘ 𝑀 ) ∈ V ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) )
15	2 4 14	syl2anc	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) )
16	1 2 3	mnringscad	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )
17		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18	1 9 5 2 3	mnringvscad	⊢ ( 𝜑 → ( ·𝑠 ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) = ( ·𝑠 ‘ 𝐹 ) )
19	18	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐹 ) 𝑦 ) )
20	8 11 13 15 16 17 19	lmodpropd	⊢ ( 𝜑 → ( ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ∈ LMod ↔ 𝐹 ∈ LMod ) )
21	7 20	mpbid	⊢ ( 𝜑 → 𝐹 ∈ LMod )