Theorem frlmelbas

Description: Membership in the base set of the free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 23-Jun-2019)

	Ref	Expression
Hypotheses	frlmval.f	|- F = ( R freeLMod I )
	frlmelbas.n	|- N = ( Base ` R )
	frlmelbas.z	|- .0. = ( 0g ` R )
	frlmelbas.b	|- B = ( Base ` F )
Assertion	frlmelbas	|- ( ( R e. V /\ I e. W ) -> ( X e. B <-> ( X e. ( N ^m I ) /\ X finSupp .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	|- F = ( R freeLMod I )
2		frlmelbas.n	|- N = ( Base ` R )
3		frlmelbas.z	|- .0. = ( 0g ` R )
4		frlmelbas.b	|- B = ( Base ` F )
5		eqid	|- { k e. ( N ^m I ) | k finSupp .0. } = { k e. ( N ^m I ) | k finSupp .0. }
6	1 2 3 5	frlmbas	|- ( ( R e. V /\ I e. W ) -> { k e. ( N ^m I ) | k finSupp .0. } = ( Base ` F ) )
7	4 6	eqtr4id	|- ( ( R e. V /\ I e. W ) -> B = { k e. ( N ^m I ) | k finSupp .0. } )
8	7	eleq2d	|- ( ( R e. V /\ I e. W ) -> ( X e. B <-> X e. { k e. ( N ^m I ) | k finSupp .0. } ) )
9		breq1	|- ( k = X -> ( k finSupp .0. <-> X finSupp .0. ) )
10	9	elrab	|- ( X e. { k e. ( N ^m I ) | k finSupp .0. } <-> ( X e. ( N ^m I ) /\ X finSupp .0. ) )
11	8 10	bitrdi	|- ( ( R e. V /\ I e. W ) -> ( X e. B <-> ( X e. ( N ^m I ) /\ X finSupp .0. ) ) )