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

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		simpr	$$⊢\left(I\in W\wedge X\in B\right)\to X\in B$$
5	1 3	frlmrcl	$$⊢X\in B\to R\in \mathrm{V}$$
6		simpl	$$⊢\left(I\in W\wedge X\in B\right)\to I\in W$$
7		eqid	$$⊢0_R=0_R$$
8	1 2 7 3	frlmelbas	$$⊢\left(R\in \mathrm{V}\wedge I\in W\right)\to \left(X\in B\leftrightarrow \left(X\in \left(N^I\right)\wedge {finSupp}_{0_R}\left(X\right)\right)\right)$$
9	5 6 8	syl2an2	$$⊢\left(I\in W\wedge X\in B\right)\to \left(X\in B\leftrightarrow \left(X\in \left(N^I\right)\wedge {finSupp}_{0_R}\left(X\right)\right)\right)$$
10	4 9	mpbid	$$⊢\left(I\in W\wedge X\in B\right)\to \left(X\in \left(N^I\right)\wedge {finSupp}_{0_R}\left(X\right)\right)$$
11	10	simpld	$$⊢\left(I\in W\wedge X\in B\right)\to X\in \left(N^I\right)$$