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	⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion	linds1	⊢ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) → 𝑋 ⊆ 𝐵 )

Proof

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