Theorem mnringscad

Description: The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024) (Proof shortened by AV, 1-Nov-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		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
9		scandxnmulrndx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
10		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
11	1 8 9 10 5 2 3	mnringnmulrd	$$⊢\phi \to \mathrm{Scalar}\left(R\mathrm{freeLMod}{\mathrm{Base}}_M\right)=\mathrm{Scalar}\left(F\right)$$
12	7 11	eqtrd	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$