Theorem mnringbased

Description: The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024) (Proof shortened by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	mnringbased.1	|- F = ( R MndRing M )
	mnringbased.2	|- A = ( Base ` M )
	mnringbased.3	|- V = ( R freeLMod A )
	mnringbased.4	|- B = ( Base ` V )
	mnringbased.5	|- ( ph -> R e. U )
	mnringbased.6	|- ( ph -> M e. W )
Assertion	mnringbased	|- ( ph -> B = ( Base ` F ) )

Proof

Step	Hyp	Ref	Expression
1		mnringbased.1	|- F = ( R MndRing M )
2		mnringbased.2	|- A = ( Base ` M )
3		mnringbased.3	|- V = ( R freeLMod A )
4		mnringbased.4	|- B = ( Base ` V )
5		mnringbased.5	|- ( ph -> R e. U )
6		mnringbased.6	|- ( ph -> M e. W )
7		baseid	|- Base = Slot ( Base ` ndx )
8		basendxnmulrndx	|- ( Base ` ndx ) =/= ( .r ` ndx )
9	1 7 8 2 3 5 6	mnringnmulrd	|- ( ph -> ( Base ` V ) = ( Base ` F ) )
10	4 9	eqtrid	|- ( ph -> B = ( Base ` F ) )