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	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringbaserd.2	$$⊢B={\mathrm{Base}}_F$$
	mnringbaserd.3	$$⊢A={\mathrm{Base}}_M$$
	mnringbaserd.4	$$⊢V=R\mathrm{freeLMod}A$$
	mnringbaserd.5	$$⊢\phi \to R\in U$$
	mnringbaserd.6	$$⊢\phi \to M\in W$$
Assertion	mnringbaserd	$$⊢\phi \to B={\mathrm{Base}}_V$$

Proof

Step	Hyp	Ref	Expression
1		mnringbaserd.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringbaserd.2	$$⊢B={\mathrm{Base}}_F$$
3		mnringbaserd.3	$$⊢A={\mathrm{Base}}_M$$
4		mnringbaserd.4	$$⊢V=R\mathrm{freeLMod}A$$
5		mnringbaserd.5	$$⊢\phi \to R\in U$$
6		mnringbaserd.6	$$⊢\phi \to M\in W$$
7		eqid	$$⊢{\mathrm{Base}}_V={\mathrm{Base}}_V$$
8	1 3 4 7 5 6	mnringbased	$$⊢\phi \to {\mathrm{Base}}_V={\mathrm{Base}}_F$$
9	2 8	eqtr4id	$$⊢\phi \to B={\mathrm{Base}}_V$$