Theorem mnringbaserd

Description: The base set of a monoid ring. Converse of mnringbased . (Contributed by Rohan Ridenour, 14-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		mnringbaserd.1	|- F = ( R MndRing M )
2		mnringbaserd.2	|- B = ( Base ` F )
3		mnringbaserd.3	|- A = ( Base ` M )
4		mnringbaserd.4	|- V = ( R freeLMod A )
5		mnringbaserd.5	|- ( ph -> R e. U )
6		mnringbaserd.6	|- ( ph -> M e. W )
7		eqid	|- ( Base ` V ) = ( Base ` V )
8	1 3 4 7 5 6	mnringbased	|- ( ph -> ( Base ` V ) = ( Base ` F ) )
9	2 8	eqtr4id	|- ( ph -> B = ( Base ` V ) )