Theorem mnringelbased

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

	Ref	Expression
Hypotheses	mnringelbased.1	|- F = ( R MndRing M )
	mnringelbased.2	|- B = ( Base ` F )
	mnringelbased.3	|- A = ( Base ` M )
	mnringelbased.4	|- C = ( Base ` R )
	mnringelbased.5	|- .0. = ( 0g ` R )
	mnringelbased.6	|- ( ph -> R e. U )
	mnringelbased.7	|- ( ph -> M e. W )
Assertion	mnringelbased	|- ( ph -> ( X e. B <-> ( X e. ( C ^m A ) /\ X finSupp .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnringelbased.1	|- F = ( R MndRing M )
2		mnringelbased.2	|- B = ( Base ` F )
3		mnringelbased.3	|- A = ( Base ` M )
4		mnringelbased.4	|- C = ( Base ` R )
5		mnringelbased.5	|- .0. = ( 0g ` R )
6		mnringelbased.6	|- ( ph -> R e. U )
7		mnringelbased.7	|- ( ph -> M e. W )
8		eqid	|- ( R freeLMod A ) = ( R freeLMod A )
9	1 2 3 8 6 7	mnringbaserd	|- ( ph -> B = ( Base ` ( R freeLMod A ) ) )
10	9	eleq2d	|- ( ph -> ( X e. B <-> X e. ( Base ` ( R freeLMod A ) ) ) )
11	3	fvexi	|- A e. _V
12		eqid	|- ( Base ` ( R freeLMod A ) ) = ( Base ` ( R freeLMod A ) )
13	8 4 5 12	frlmelbas	|- ( ( R e. U /\ A e. _V ) -> ( X e. ( Base ` ( R freeLMod A ) ) <-> ( X e. ( C ^m A ) /\ X finSupp .0. ) ) )
14	6 11 13	sylancl	|- ( ph -> ( X e. ( Base ` ( R freeLMod A ) ) <-> ( X e. ( C ^m A ) /\ X finSupp .0. ) ) )
15	10 14	bitrd	|- ( ph -> ( X e. B <-> ( X e. ( C ^m A ) /\ X finSupp .0. ) ) )