Metamath Proof Explorer

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 ∈ LIndS ⁡ W → I ↾ X LIndF W

Proof

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