Theorem frlmelbas

Description: Membership in the base set of the free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 23-Jun-2019)

	Ref	Expression
Hypotheses	frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmelbas.n	$$⊢N={\mathrm{Base}}_R$$
	frlmelbas.z	$$⊢\underset{\dot{}}{0}=0_R$$
	frlmelbas.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	frlmelbas	$$⊢\left(R\in V\wedge I\in W\right)\to \left(X\in B\leftrightarrow \left(X\in \left(N^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmelbas.n	$$⊢N={\mathrm{Base}}_R$$
3		frlmelbas.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		frlmelbas.b	$$⊢B={\mathrm{Base}}_F$$
5		eqid	$$⊢\left\{k\in \left(N^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(k\right)\right\}=\left\{k\in \left(N^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(k\right)\right\}$$
6	1 2 3 5	frlmbas	$$⊢\left(R\in V\wedge I\in W\right)\to \left\{k\in \left(N^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(k\right)\right\}={\mathrm{Base}}_F$$
7	4 6	eqtr4id	$$⊢\left(R\in V\wedge I\in W\right)\to B=\left\{k\in \left(N^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(k\right)\right\}$$
8	7	eleq2d	$$⊢\left(R\in V\wedge I\in W\right)\to \left(X\in B\leftrightarrow X\in \left\{k\in \left(N^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(k\right)\right\}\right)$$
9		breq1	$$⊢k=X\to \left({finSupp}_{\underset{\dot{}}{0}}\left(k\right)\leftrightarrow {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
10	9	elrab	$$⊢X\in \left\{k\in \left(N^I\right)|{finSupp}_{\underset{\dot{}}{0}}\left(k\right)\right\}\leftrightarrow \left(X\in \left(N^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
11	8 10	bitrdi	$$⊢\left(R\in V\wedge I\in W\right)\to \left(X\in B\leftrightarrow \left(X\in \left(N^I\right)\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)$$