Metamath Proof Explorer

Theorem f1linds

Description: A family constructed from non-repeated elements of an independent set is independent. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Assertion f1linds 
|- ( ( W e. LMod /\ S e. ( LIndS ` W ) /\ F : D -1-1-> S ) -> F LIndF W )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : D -1-1-> S -> F : D --> S )
2 fcoi2 
 |-  ( F : D --> S -> ( ( _I |` S ) o. F ) = F )
3 1 2 syl 
 |-  ( F : D -1-1-> S -> ( ( _I |` S ) o. F ) = F )
4 3 3ad2ant3 
 |-  ( ( W e. LMod /\ S e. ( LIndS ` W ) /\ F : D -1-1-> S ) -> ( ( _I |` S ) o. F ) = F )
5 simp1 
 |-  ( ( W e. LMod /\ S e. ( LIndS ` W ) /\ F : D -1-1-> S ) -> W e. LMod )
6 linds2 
 |-  ( S e. ( LIndS ` W ) -> ( _I |` S ) LIndF W )
7 6 3ad2ant2 
 |-  ( ( W e. LMod /\ S e. ( LIndS ` W ) /\ F : D -1-1-> S ) -> ( _I |` S ) LIndF W )
8 dmresi 
 |-  dom ( _I |` S ) = S
9 f1eq3 
 |-  ( dom ( _I |` S ) = S -> ( F : D -1-1-> dom ( _I |` S ) <-> F : D -1-1-> S ) )
10 8 9 ax-mp 
 |-  ( F : D -1-1-> dom ( _I |` S ) <-> F : D -1-1-> S )
11 10 biimpri 
 |-  ( F : D -1-1-> S -> F : D -1-1-> dom ( _I |` S ) )
12 11 3ad2ant3 
 |-  ( ( W e. LMod /\ S e. ( LIndS ` W ) /\ F : D -1-1-> S ) -> F : D -1-1-> dom ( _I |` S ) )
13 f1lindf 
 |-  ( ( W e. LMod /\ ( _I |` S ) LIndF W /\ F : D -1-1-> dom ( _I |` S ) ) -> ( ( _I |` S ) o. F ) LIndF W )
14 5 7 12 13 syl3anc 
 |-  ( ( W e. LMod /\ S e. ( LIndS ` W ) /\ F : D -1-1-> S ) -> ( ( _I |` S ) o. F ) LIndF W )
15 4 14 eqbrtrrd 
 |-  ( ( W e. LMod /\ S e. ( LIndS ` W ) /\ F : D -1-1-> S ) -> F LIndF W )