Theorem frlmbasmap

Description: Elements of the free module are set functions. (Contributed by Stefan O'Rear, 3-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	frlmval.f	|- F = ( R freeLMod I )
	frlmbasmap.n	|- N = ( Base ` R )
	frlmbasmap.b	|- B = ( Base ` F )
Assertion	frlmbasmap	|- ( ( I e. W /\ X e. B ) -> X e. ( N ^m I ) )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	|- F = ( R freeLMod I )
2		frlmbasmap.n	|- N = ( Base ` R )
3		frlmbasmap.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	|- ( 0g ` R ) = ( 0g ` R )
8	1 2 7 3	frlmelbas	|- ( ( R e. _V /\ I e. W ) -> ( X e. B <-> ( X e. ( N ^m I ) /\ X finSupp ( 0g ` R ) ) ) )
9	5 6 8	syl2an2	|- ( ( I e. W /\ X e. B ) -> ( X e. B <-> ( X e. ( N ^m I ) /\ X finSupp ( 0g ` R ) ) ) )
10	4 9	mpbid	|- ( ( I e. W /\ X e. B ) -> ( X e. ( N ^m I ) /\ X finSupp ( 0g ` R ) ) )
11	10	simpld	|- ( ( I e. W /\ X e. B ) -> X e. ( N ^m I ) )