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	⊢ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) → ( I ↾ 𝑋 ) LIndF 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) → 𝑊 ∈ dom LIndS )
2		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3	2	islinds	⊢ ( 𝑊 ∈ dom LIndS → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋 ⊆ ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) )
4	1 3	syl	⊢ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋 ⊆ ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) )
5	4	ibi	⊢ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) → ( 𝑋 ⊆ ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) )
6	5	simprd	⊢ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) → ( I ↾ 𝑋 ) LIndF 𝑊 )