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	|- F = ( R MndRing M )
	mnringscad.2	|- ( ph -> R e. U )
	mnringscad.3	|- ( ph -> M e. W )
Assertion	mnringscad	|- ( ph -> R = ( Scalar ` F ) )

Proof

Step	Hyp	Ref	Expression
1		mnringscad.1	|- F = ( R MndRing M )
2		mnringscad.2	|- ( ph -> R e. U )
3		mnringscad.3	|- ( ph -> M e. W )
4		fvex	|- ( Base ` M ) e. _V
5		eqid	|- ( R freeLMod ( Base ` M ) ) = ( R freeLMod ( Base ` M ) )
6	5	frlmsca	|- ( ( R e. U /\ ( Base ` M ) e. _V ) -> R = ( Scalar ` ( R freeLMod ( Base ` M ) ) ) )
7	2 4 6	sylancl	|- ( ph -> R = ( Scalar ` ( R freeLMod ( Base ` M ) ) ) )
8		scaid	|- Scalar = Slot ( Scalar ` ndx )
9		scandxnmulrndx	|- ( Scalar ` ndx ) =/= ( .r ` ndx )
10		eqid	|- ( Base ` M ) = ( Base ` M )
11	1 8 9 10 5 2 3	mnringnmulrd	|- ( ph -> ( Scalar ` ( R freeLMod ( Base ` M ) ) ) = ( Scalar ` F ) )
12	7 11	eqtrd	|- ( ph -> R = ( Scalar ` F ) )