Theorem mnringelbased

Description: Membership in the base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringelbased.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringelbased.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
	mnringelbased.3	⊢ 𝐴 = ( Base ‘ 𝑀 )
	mnringelbased.4	⊢ 𝐶 = ( Base ‘ 𝑅 )
	mnringelbased.5	⊢ 0 = ( 0g ‘ 𝑅 )
	mnringelbased.6	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	mnringelbased.7	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
Assertion	mnringelbased	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝑋 finSupp 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnringelbased.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringelbased.2	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		mnringelbased.3	⊢ 𝐴 = ( Base ‘ 𝑀 )
4		mnringelbased.4	⊢ 𝐶 = ( Base ‘ 𝑅 )
5		mnringelbased.5	⊢ 0 = ( 0g ‘ 𝑅 )
6		mnringelbased.6	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
7		mnringelbased.7	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
8		eqid	⊢ ( 𝑅 freeLMod 𝐴 ) = ( 𝑅 freeLMod 𝐴 )
9	1 2 3 8 6 7	mnringbaserd	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) )
10	9	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ) )
11	3	fvexi	⊢ 𝐴 ∈ V
12		eqid	⊢ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐴 ) )
13	8 4 5 12	frlmelbas	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝐴 ∈ V ) → ( 𝑋 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↔ ( 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝑋 finSupp 0 ) ) )
14	6 11 13	sylancl	⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ ( 𝑅 freeLMod 𝐴 ) ) ↔ ( 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝑋 finSupp 0 ) ) )
15	10 14	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝑋 finSupp 0 ) ) )