Theorem mnringbasefd

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

	Ref	Expression
Hypotheses	mnringbasefd.1	No typesetting found for |- F = ( R MndRing M ) with typecode |-
	mnringbasefd.2	$$⊢B={\mathrm{Base}}_F$$
	mnringbasefd.3	$$⊢A={\mathrm{Base}}_M$$
	mnringbasefd.4	$$⊢C={\mathrm{Base}}_R$$
	mnringbasefd.5	$$⊢\phi \to R\in U$$
	mnringbasefd.6	$$⊢\phi \to M\in W$$
	mnringbasefd.7	$$⊢\phi \to X\in B$$
Assertion	mnringbasefd	$$⊢\phi \to X:A⟶C$$

Proof

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