Theorem mnringbasefsuppd

Description: Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringbasefsuppd.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringbasefsuppd.2	$$⊢B={\mathrm{Base}}_F$$
	mnringbasefsuppd.3	$$⊢\underset{\dot{}}{0}=0_R$$
	mnringbasefsuppd.4	$$⊢\phi \to R\in U$$
	mnringbasefsuppd.5	$$⊢\phi \to M\in W$$
	mnringbasefsuppd.6	$$⊢\phi \to X\in B$$
Assertion	mnringbasefsuppd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		mnringbasefsuppd.1	Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2		mnringbasefsuppd.2	$$⊢B={\mathrm{Base}}_F$$
3		mnringbasefsuppd.3	$$⊢\underset{\dot{}}{0}=0_R$$
4		mnringbasefsuppd.4	$$⊢\phi \to R\in U$$
5		mnringbasefsuppd.5	$$⊢\phi \to M\in W$$
6		mnringbasefsuppd.6	$$⊢\phi \to X\in B$$
7		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
8		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
9	1 2 7 8 3 4 5	mnringelbased	$$⊢\phi \to \left(X\in B\leftrightarrow \left(X\in \left({{\mathrm{Base}}_R}^{{\mathrm{Base}}_M}\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$
10	6 9	mpbid	$$⊢\phi \to \left(X\in \left({{\mathrm{Base}}_R}^{{\mathrm{Base}}_M}\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
11	10	simprd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(X\right)$$