Theorem mnringscad

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

	Ref	Expression
Hypotheses	mnringscad.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringscad.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	mnringscad.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
Assertion	mnringscad	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		mnringscad.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringscad.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
3		mnringscad.3	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
4		fvex	⊢ ( Base ‘ 𝑀 ) ∈ V
5		eqid	⊢ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) = ( 𝑅 freeLMod ( Base ‘ 𝑀 ) )
6	5	frlmsca	⊢ ( ( 𝑅 ∈ 𝑈 ∧ ( Base ‘ 𝑀 ) ∈ V ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) )
7	2 4 6	sylancl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) )
8		df-sca	⊢ Scalar = Slot 5
9		5nn	⊢ 5 ∈ ℕ
10		3re	⊢ 3 ∈ ℝ
11		3lt5	⊢ 3 < 5
12	10 11	gtneii	⊢ 5 ≠ 3
13		mulrndx	⊢ ( .r ‘ ndx ) = 3
14	12 13	neeqtrri	⊢ 5 ≠ ( .r ‘ ndx )
15		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
16	1 8 9 14 15 5 2 3	mnringnmulrd	⊢ ( 𝜑 → ( Scalar ‘ ( 𝑅 freeLMod ( Base ‘ 𝑀 ) ) ) = ( Scalar ‘ 𝐹 ) )
17	7 16	eqtrd	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )