Theorem mnringscad

Description: The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-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		df-sca	|- Scalar = Slot 5
9		5nn	|- 5 e. NN
10		3re	|- 3 e. RR
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 ` M ) = ( Base ` M )
16	1 8 9 14 15 5 2 3	mnringnmulrd	|- ( ph -> ( Scalar ` ( R freeLMod ( Base ` M ) ) ) = ( Scalar ` F ) )
17	7 16	eqtrd	|- ( ph -> R = ( Scalar ` F ) )