Theorem mnringbasefsuppd

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

	Ref	Expression
Hypotheses	mnringbasefsuppd.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringbasefsuppd.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
	mnringbasefsuppd.3	⊢ 0 = ( 0g ‘ 𝑅 )
	mnringbasefsuppd.4	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	mnringbasefsuppd.5	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
	mnringbasefsuppd.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	mnringbasefsuppd	⊢ ( 𝜑 → 𝑋 finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		mnringbasefsuppd.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringbasefsuppd.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		mnringbasefsuppd.3	⊢ 0 = ( 0g ‘ 𝑅 )
4		mnringbasefsuppd.4	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
5		mnringbasefsuppd.5	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
6		mnringbasefsuppd.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9	1 2 7 8 3 4 5	mnringelbased	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( Base ‘ 𝑀 ) ) ∧ 𝑋 finSupp 0 ) ) )
10	6 9	mpbid	⊢ ( 𝜑 → ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( Base ‘ 𝑀 ) ) ∧ 𝑋 finSupp 0 ) )
11	10	simprd	⊢ ( 𝜑 → 𝑋 finSupp 0 )