Theorem mnringbasefsuppd

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

	Ref	Expression
Hypotheses	mnringbasefsuppd.1	|- F = ( R MndRing M )
	mnringbasefsuppd.2	|- B = ( Base ` F )
	mnringbasefsuppd.3	|- .0. = ( 0g ` R )
	mnringbasefsuppd.4	|- ( ph -> R e. U )
	mnringbasefsuppd.5	|- ( ph -> M e. W )
	mnringbasefsuppd.6	|- ( ph -> X e. B )
Assertion	mnringbasefsuppd	|- ( ph -> X finSupp .0. )

Proof

Step	Hyp	Ref	Expression
1		mnringbasefsuppd.1	|- F = ( R MndRing M )
2		mnringbasefsuppd.2	|- B = ( Base ` F )
3		mnringbasefsuppd.3	|- .0. = ( 0g ` R )
4		mnringbasefsuppd.4	|- ( ph -> R e. U )
5		mnringbasefsuppd.5	|- ( ph -> M e. W )
6		mnringbasefsuppd.6	|- ( ph -> X e. B )
7		eqid	|- ( Base ` M ) = ( Base ` M )
8		eqid	|- ( Base ` R ) = ( Base ` R )
9	1 2 7 8 3 4 5	mnringelbased	|- ( ph -> ( X e. B <-> ( X e. ( ( Base ` R ) ^m ( Base ` M ) ) /\ X finSupp .0. ) ) )
10	6 9	mpbid	|- ( ph -> ( X e. ( ( Base ` R ) ^m ( Base ` M ) ) /\ X finSupp .0. ) )
11	10	simprd	|- ( ph -> X finSupp .0. )