Theorem linds2

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

	Ref	Expression
Assertion	linds2	$$⊢X\in \mathrm{LIndS}\left(W\right)\to \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢X\in \mathrm{LIndS}\left(W\right)\to W\in \mathrm{dom}\mathrm{LIndS}$$
2		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
3	2	islinds	$$⊢W\in \mathrm{dom}\mathrm{LIndS}\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(X\subseteq {\mathrm{Base}}_W\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)\right)$$
4	1 3	syl	$$⊢X\in \mathrm{LIndS}\left(W\right)\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(X\subseteq {\mathrm{Base}}_W\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 {\mathrm{Base}}_W\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)$$
6	5	simprd	$$⊢X\in \mathrm{LIndS}\left(W\right)\to \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W$$