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 ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐺 ⊆ 𝐹 ) → 𝐺 ∈ ( LIndS ‘ 𝑊 ) )

Proof

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