Theorem mnringelbased

Description: Membership in the base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringelbased.1	$$⊢F=R\mathrm{MndRing}M$$
	mnringelbased.2	$$⊢B={\mathrm{Base}}_F$$
	mnringelbased.3	$$⊢A={\mathrm{Base}}_M$$
	mnringelbased.4	$$⊢C={\mathrm{Base}}_R$$
	mnringelbased.5	$$⊢\underset{\dot{}}{0}=0_R$$
	mnringelbased.6	$$⊢\phi \to R\in U$$
	mnringelbased.7	$$⊢\phi \to M\in W$$
Assertion	mnringelbased	$$⊢\phi \to \left(X\in B\leftrightarrow \left(X\in \left(C^A\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mnringelbased.1	$$⊢F=R\mathrm{MndRing}M$$
2		mnringelbased.2	$$⊢B={\mathrm{Base}}_F$$
3		mnringelbased.3	$$⊢A={\mathrm{Base}}_M$$
4		mnringelbased.4	$$⊢C={\mathrm{Base}}_R$$
5		mnringelbased.5	$$⊢\underset{\dot{}}{0}=0_R$$
6		mnringelbased.6	$$⊢\phi \to R\in U$$
7		mnringelbased.7	$$⊢\phi \to M\in W$$
8		eqid	$$⊢R\mathrm{freeLMod}A=R\mathrm{freeLMod}A$$
9	1 2 3 8 6 7	mnringbaserd	$$⊢\phi \to B={\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}$$
10	9	eleq2d	$$⊢\phi \to \left(X\in B\leftrightarrow X\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}\right)$$
11	3	fvexi	$$⊢A\in \mathrm{V}$$
12		eqid	$$⊢{\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}={\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}$$
13	8 4 5 12	frlmelbas	$$⊢\left(R\in U\wedge A\in \mathrm{V}\right)\to \left(X\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}\leftrightarrow \left(X\in \left(C^A\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$
14	6 11 13	sylancl	$$⊢\phi \to \left(X\in {\mathrm{Base}}_{\left(R\mathrm{freeLMod}A\right)}\leftrightarrow \left(X\in \left(C^A\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$
15	10 14	bitrd	$$⊢\phi \to \left(X\in B\leftrightarrow \left(X\in \left(C^A\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$