Theorem linds1

Description: An independent set of vectors is a set of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypothesis	islinds.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	linds1	$$⊢X\in \mathrm{LIndS}\left(W\right)\to X\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		islinds.b	$$⊢B={\mathrm{Base}}_W$$
2		elfvdm	$$⊢X\in \mathrm{LIndS}\left(W\right)\to W\in \mathrm{dom}\mathrm{LIndS}$$
3	1	islinds	$$⊢W\in \mathrm{dom}\mathrm{LIndS}\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(X\subseteq B\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)\right)$$
4	2 3	syl	$$⊢X\in \mathrm{LIndS}\left(W\right)\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(X\subseteq B\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)\right)$$
5	4	ibi	$$⊢X\in \mathrm{LIndS}\left(W\right)\to \left(X\subseteq B\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)$$
6	5	simpld	$$⊢X\in \mathrm{LIndS}\left(W\right)\to X\subseteq B$$