This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lindsss

Description: Any subset of an independent set is independent. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion lindsss ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → G ∈ LIndS ⁡ W

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base W = Base W
2 1 linds1 ⊢ F ∈ LIndS ⁡ W → F ⊆ Base W
3 2 adantl ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W → F ⊆ Base W
4 sstr2 ⊢ G ⊆ F → F ⊆ Base W → G ⊆ Base W
5 3 4 syl5com ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W → G ⊆ F → G ⊆ Base W
6 5 3impia ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → G ⊆ Base W
7 simp1 ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → W ∈ LMod
8 linds2 ⊢ F ∈ LIndS ⁡ W → I ↾ F LIndF W
9 8 3ad2ant2 ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → I ↾ F LIndF W
10 lindfres ⊢ W ∈ LMod ∧ I ↾ F LIndF W → I ↾ F ↾ G LIndF W
11 7 9 10 syl2anc ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → I ↾ F ↾ G LIndF W
12 resabs1 ⊢ G ⊆ F → I ↾ F ↾ G = I ↾ G
13 12 breq1d ⊢ G ⊆ F → I ↾ F ↾ G LIndF W ↔ I ↾ G LIndF W
14 13 3ad2ant3 ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → I ↾ F ↾ G LIndF W ↔ I ↾ G LIndF W
15 11 14 mpbid ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → I ↾ G LIndF W
16 1 islinds ⊢ W ∈ LMod → G ∈ LIndS ⁡ W ↔ G ⊆ Base W ∧ I ↾ G LIndF W
17 16 3ad2ant1 ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → G ∈ LIndS ⁡ W ↔ G ⊆ Base W ∧ I ↾ G LIndF W
18 6 15 17 mpbir2and ⊢ W ∈ LMod ∧ F ∈ LIndS ⁡ W ∧ G ⊆ F → G ∈ LIndS ⁡ W