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 e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> G e. ( LIndS ` W ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` W ) = ( Base ` W )
2 1 linds1 
 |-  ( F e. ( LIndS ` W ) -> F C_ ( Base ` W ) )
3 2 adantl 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) ) -> F C_ ( Base ` W ) )
4 sstr2 
 |-  ( G C_ F -> ( F C_ ( Base ` W ) -> G C_ ( Base ` W ) ) )
5 3 4 syl5com 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) ) -> ( G C_ F -> G C_ ( Base ` W ) ) )
6 5 3impia 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> G C_ ( Base ` W ) )
7 simp1 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> W e. LMod )
8 linds2 
 |-  ( F e. ( LIndS ` W ) -> ( _I |` F ) LIndF W )
9 8 3ad2ant2 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> ( _I |` F ) LIndF W )
10 lindfres 
 |-  ( ( W e. LMod /\ ( _I |` F ) LIndF W ) -> ( ( _I |` F ) |` G ) LIndF W )
11 7 9 10 syl2anc 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> ( ( _I |` F ) |` G ) LIndF W )
12 resabs1 
 |-  ( G C_ F -> ( ( _I |` F ) |` G ) = ( _I |` G ) )
13 12 breq1d 
 |-  ( G C_ F -> ( ( ( _I |` F ) |` G ) LIndF W <-> ( _I |` G ) LIndF W ) )
14 13 3ad2ant3 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> ( ( ( _I |` F ) |` G ) LIndF W <-> ( _I |` G ) LIndF W ) )
15 11 14 mpbid 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> ( _I |` G ) LIndF W )
16 1 islinds 
 |-  ( W e. LMod -> ( G e. ( LIndS ` W ) <-> ( G C_ ( Base ` W ) /\ ( _I |` G ) LIndF W ) ) )
17 16 3ad2ant1 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> ( G e. ( LIndS ` W ) <-> ( G C_ ( Base ` W ) /\ ( _I |` G ) LIndF W ) ) )
18 6 15 17 mpbir2and 
 |-  ( ( W e. LMod /\ F e. ( LIndS ` W ) /\ G C_ F ) -> G e. ( LIndS ` W ) )