Theorem frlmbasfsupp

Description: Elements of the free module are finitely supported. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Thierry Arnoux, 21-Jun-2019) (Proof shortened by AV, 20-Jul-2019)

	Ref	Expression
Hypotheses	frlmval.f	|- F = ( R freeLMod I )
	frlmbasfsupp.z	|- .0. = ( 0g ` R )
	frlmbasfsupp.b	|- B = ( Base ` F )
Assertion	frlmbasfsupp	|- ( ( I e. W /\ X e. B ) -> X finSupp .0. )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	|- F = ( R freeLMod I )
2		frlmbasfsupp.z	|- .0. = ( 0g ` R )
3		frlmbasfsupp.b	|- B = ( Base ` F )
4		simpr	|- ( ( I e. W /\ X e. B ) -> X e. B )
5	1 3	frlmrcl	|- ( X e. B -> R e. _V )
6		simpl	|- ( ( I e. W /\ X e. B ) -> I e. W )
7		eqid	|- ( Base ` R ) = ( Base ` R )
8	1 7 2 3	frlmelbas	|- ( ( R e. _V /\ I e. W ) -> ( X e. B <-> ( X e. ( ( Base ` R ) ^m I ) /\ X finSupp .0. ) ) )
9	5 6 8	syl2an2	|- ( ( I e. W /\ X e. B ) -> ( X e. B <-> ( X e. ( ( Base ` R ) ^m I ) /\ X finSupp .0. ) ) )
10	4 9	mpbid	|- ( ( I e. W /\ X e. B ) -> ( X e. ( ( Base ` R ) ^m I ) /\ X finSupp .0. ) )
11	10	simprd	|- ( ( I e. W /\ X e. B ) -> X finSupp .0. )