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 e. ( LIndS ` W ) -> ( _I |` X ) LIndF W )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	|- ( X e. ( LIndS ` W ) -> W e. dom LIndS )
2		eqid	|- ( Base ` W ) = ( Base ` W )
3	2	islinds	|- ( W e. dom LIndS -> ( X e. ( LIndS ` W ) <-> ( X C_ ( Base ` W ) /\ ( _I |` X ) LIndF W ) ) )
4	1 3	syl	|- ( X e. ( LIndS ` W ) -> ( X e. ( LIndS ` W ) <-> ( X C_ ( Base ` W ) /\ ( _I |` X ) LIndF W ) ) )
5	4	ibi	|- ( X e. ( LIndS ` W ) -> ( X C_ ( Base ` W ) /\ ( _I |` X ) LIndF W ) )
6	5	simprd	|- ( X e. ( LIndS ` W ) -> ( _I |` X ) LIndF W )