Metamath Proof Explorer

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 = Base W
Assertion linds1 ⊢ X ∈ LIndS ⁡ W → X ⊆ B

Proof

Step Hyp Ref Expression
1 islinds.b ⊢ B = Base W
2 elfvdm ⊢ X ∈ LIndS ⁡ W → W ∈ dom ⁡ LIndS
3 1 islinds ⊢ W ∈ dom ⁡ LIndS → X ∈ LIndS ⁡ W ↔ X ⊆ B ∧ I ↾ X LIndF W
4 2 3 syl ⊢ X ∈ LIndS ⁡ W → X ∈ LIndS ⁡ W ↔ X ⊆ B ∧ I ↾ X LIndF W
5 4 ibi ⊢ X ∈ LIndS ⁡ W → X ⊆ B ∧ I ↾ X LIndF W
6 5 simpld ⊢ X ∈ LIndS ⁡ W → X ⊆ B