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\mathrm{freeLMod}I$$
	frlmbasmap.n	$$⊢N={\mathrm{Base}}_R$$
	frlmbasmap.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	frlmbasf	$$⊢\left(I\in W\wedge X\in B\right)\to X:I⟶N$$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmbasmap.n	$$⊢N={\mathrm{Base}}_R$$
3		frlmbasmap.b	$$⊢B={\mathrm{Base}}_F$$
4	1 2 3	frlmbasmap	$$⊢\left(I\in W\wedge X\in B\right)\to X\in \left(N^I\right)$$
5	2	fvexi	$$⊢N\in \mathrm{V}$$
6		elmapg	$$⊢\left(N\in \mathrm{V}\wedge I\in W\right)\to \left(X\in \left(N^I\right)\leftrightarrow X:I⟶N\right)$$
7	5 6	mpan	$$⊢I\in W\to \left(X\in \left(N^I\right)\leftrightarrow X:I⟶N\right)$$
8	7	adantr	$$⊢\left(I\in W\wedge X\in B\right)\to \left(X\in \left(N^I\right)\leftrightarrow X:I⟶N\right)$$
9	4 8	mpbid	$$⊢\left(I\in W\wedge X\in B\right)\to X:I⟶N$$