Theorem mnringbasefd

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

	Ref	Expression
Hypotheses	mnringbasefd.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringbasefd.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
	mnringbasefd.3	⊢ 𝐴 = ( Base ‘ 𝑀 )
	mnringbasefd.4	⊢ 𝐶 = ( Base ‘ 𝑅 )
	mnringbasefd.5	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	mnringbasefd.6	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
	mnringbasefd.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	mnringbasefd	⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mnringbasefd.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringbasefd.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		mnringbasefd.3	⊢ 𝐴 = ( Base ‘ 𝑀 )
4		mnringbasefd.4	⊢ 𝐶 = ( Base ‘ 𝑅 )
5		mnringbasefd.5	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
6		mnringbasefd.6	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
7		mnringbasefd.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9	1 2 3 4 8 5 6	mnringelbased	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝑋 finSupp ( 0g ‘ 𝑅 ) ) ) )
10	7 9	mpbid	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝑋 finSupp ( 0g ‘ 𝑅 ) ) )
11	10	simpld	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) )
12		elmapi	⊢ ( 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) → 𝑋 : 𝐴 ⟶ 𝐶 )
13	11 12	syl	⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐶 )