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 ‘ 𝑊 ) )