Metamath Proof Explorer

Theorem lindfres

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

Ref Expression
Assertion lindfres 
|- ( ( W e. LMod /\ F LIndF W ) -> ( F |` X ) LIndF W )

Proof

Step Hyp Ref Expression
1 coires1 
 |-  ( F o. ( _I |` dom ( F |` X ) ) ) = ( F |` dom ( F |` X ) )
2 resdmres 
 |-  ( F |` dom ( F |` X ) ) = ( F |` X )
3 1 2 eqtri 
 |-  ( F o. ( _I |` dom ( F |` X ) ) ) = ( F |` X )
4 f1oi 
 |-  ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-onto-> dom ( F |` X )
5 f1of1 
 |-  ( ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-onto-> dom ( F |` X ) -> ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-> dom ( F |` X ) )
6 4 5 ax-mp 
 |-  ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-> dom ( F |` X )
7 resss 
 |-  ( F |` X ) C_ F
8 dmss 
 |-  ( ( F |` X ) C_ F -> dom ( F |` X ) C_ dom F )
9 7 8 ax-mp 
 |-  dom ( F |` X ) C_ dom F
10 f1ss 
 |-  ( ( ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-> dom ( F |` X ) /\ dom ( F |` X ) C_ dom F ) -> ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-> dom F )
11 6 9 10 mp2an 
 |-  ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-> dom F
12 f1lindf 
 |-  ( ( W e. LMod /\ F LIndF W /\ ( _I |` dom ( F |` X ) ) : dom ( F |` X ) -1-1-> dom F ) -> ( F o. ( _I |` dom ( F |` X ) ) ) LIndF W )
13 11 12 mp3an3 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ( F o. ( _I |` dom ( F |` X ) ) ) LIndF W )
14 3 13 eqbrtrrid 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ( F |` X ) LIndF W )