Theorem mnringscad

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

	Ref	Expression
Hypotheses	mnringscad.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringscad.2	$$⊢\phi \to R\in U$$
	mnringscad.3	$$⊢\phi \to M\in W$$
Assertion	mnringscad	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		mnringscad.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringscad.2	$$⊢\phi \to R\in U$$
3		mnringscad.3	$$⊢\phi \to M\in W$$
4		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
5		eqid	$$⊢R\mathrm{freeLMod}{\mathrm{Base}}_M=R\mathrm{freeLMod}{\mathrm{Base}}_M$$
6	5	frlmsca	$$⊢\left(R\in U\wedge {\mathrm{Base}}_M\in \mathrm{V}\right)\to R=\mathrm{Scalar}\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)$$
7	2 4 6	sylancl	$$⊢\phi \to R=\mathrm{Scalar}\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)$$
8		df-sca	$$⊢\mathrm{Scalar}=\mathrm{Slot}5$$
9		5nn	$$⊢5\in \mathbb{N}$$
10		3re	$$⊢3\in ℝ$$
11		3lt5	$$⊢3<5$$
12	10 11	gtneii	$$⊢5\ne 3$$
13		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
14	12 13	neeqtrri	$$⊢5\ne {\cdot }_{\mathrm{ndx}}$$
15		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
16	1 8 9 14 15 5 2 3	mnringnmulrd	$$⊢\phi \to \mathrm{Scalar}\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)=\mathrm{Scalar}\left(F\right)$$
17	7 16	eqtrd	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$