Theorem mnringbasefd

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

	Ref	Expression
Hypotheses	mnringbasefd.1	|- F = ( R MndRing M )
	mnringbasefd.2	|- B = ( Base ` F )
	mnringbasefd.3	|- A = ( Base ` M )
	mnringbasefd.4	|- C = ( Base ` R )
	mnringbasefd.5	|- ( ph -> R e. U )
	mnringbasefd.6	|- ( ph -> M e. W )
	mnringbasefd.7	|- ( ph -> X e. B )
Assertion	mnringbasefd	|- ( ph -> X : A --> C )

Proof

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