Theorem frlmbasf

Description: Elements of the free module are functions. (Contributed by Stefan O'Rear, 3-Feb-2015)

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

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	1 2 3	frlmbasmap	|- ( ( I e. W /\ X e. B ) -> X e. ( N ^m I ) )
5	2	fvexi	|- N e. _V
6		elmapg	|- ( ( N e. _V /\ I e. W ) -> ( X e. ( N ^m I ) <-> X : I --> N ) )
7	5 6	mpan	|- ( I e. W -> ( X e. ( N ^m I ) <-> X : I --> N ) )
8	7	adantr	|- ( ( I e. W /\ X e. B ) -> ( X e. ( N ^m I ) <-> X : I --> N ) )
9	4 8	mpbid	|- ( ( I e. W /\ X e. B ) -> X : I --> N )