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\mathrm{MndRing}M$$
	mnringbased.2	$$⊢A={\mathrm{Base}}_M$$
	mnringbased.3	$$⊢V=R\mathrm{freeLMod}A$$
	mnringbased.4	$$⊢B={\mathrm{Base}}_V$$
	mnringbased.5	$$⊢\phi \to R\in U$$
	mnringbased.6	$$⊢\phi \to M\in W$$
Assertion	mnringbased	$$⊢\phi \to B={\mathrm{Base}}_F$$

Proof

Step	Hyp	Ref	Expression
1		mnringbased.1	$$⊢F=R\mathrm{MndRing}M$$
2		mnringbased.2	$$⊢A={\mathrm{Base}}_M$$
3		mnringbased.3	$$⊢V=R\mathrm{freeLMod}A$$
4		mnringbased.4	$$⊢B={\mathrm{Base}}_V$$
5		mnringbased.5	$$⊢\phi \to R\in U$$
6		mnringbased.6	$$⊢\phi \to M\in W$$
7		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
8		basendxnmulrndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
9	1 7 8 2 3 5 6	mnringnmulrd	$$⊢\phi \to {\mathrm{Base}}_V={\mathrm{Base}}_F$$
10	4 9	eqtrid	$$⊢\phi \to B={\mathrm{Base}}_F$$