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\mathrm{freeLMod}I$$
	frlmbasfsupp.z	$$⊢\underset{\dot{}}{0}=0_R$$
	frlmbasfsupp.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	frlmbasfsupp	$$⊢\left(I\in W\wedge X\in B\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmbasfsupp.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		frlmbasfsupp.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	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8	1 7 2 3	frlmelbas	$$⊢\left(R\in \mathrm{V}\wedge I\in W\right)\to \left(X\in B\leftrightarrow \left(X\in \left({{\mathrm{Base}}_R}^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\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({{\mathrm{Base}}_R}^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$
10	4 9	mpbid	$$⊢\left(I\in W\wedge X\in B\right)\to \left(X\in \left({{\mathrm{Base}}_R}^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
11	10	simprd	$$⊢\left(I\in W\wedge X\in B\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(X\right)$$