Theorem mnringbased

Description: The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-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		df-base	|- Base = Slot 1
8		1nn	|- 1 e. NN
9		1re	|- 1 e. RR
10		1lt3	|- 1 < 3
11	9 10	ltneii	|- 1 =/= 3
12		mulrndx	|- ( .r ` ndx ) = 3
13	11 12	neeqtrri	|- 1 =/= ( .r ` ndx )
14	1 7 8 13 2 3 5 6	mnringnmulrd	|- ( ph -> ( Base ` V ) = ( Base ` F ) )
15	4 14	syl5eq	|- ( ph -> B = ( Base ` F ) )