Metamath Proof Explorer

Theorem islindf3

Description: In a nonzero ring, independent families can be equivalently characterized as renamings of independent sets. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypothesis islindf3.l 
|- L = ( Scalar ` W )
Assertion islindf3 
|- ( ( W e. LMod /\ L e. NzRing ) -> ( F LIndF W <-> ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) )

Proof

Step Hyp Ref Expression
1 islindf3.l 
 |-  L = ( Scalar ` W )
2 eqid 
 |-  ( Base ` W ) = ( Base ` W )
3 2 1 lindff1 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> F : dom F -1-1-> ( Base ` W ) )
4 3 3expa 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W ) -> F : dom F -1-1-> ( Base ` W ) )
5 ssv 
 |-  ( Base ` W ) C_ _V
6 f1ss 
 |-  ( ( F : dom F -1-1-> ( Base ` W ) /\ ( Base ` W ) C_ _V ) -> F : dom F -1-1-> _V )
7 4 5 6 sylancl 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W ) -> F : dom F -1-1-> _V )
8 lindfrn 
 |-  ( ( W e. LMod /\ F LIndF W ) -> ran F e. ( LIndS ` W ) )
9 8 adantlr 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W ) -> ran F e. ( LIndS ` W ) )
10 7 9 jca 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W ) -> ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) )
11 simpll 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) -> W e. LMod )
12 simprr 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) -> ran F e. ( LIndS ` W ) )
13 f1f1orn 
 |-  ( F : dom F -1-1-> _V -> F : dom F -1-1-onto-> ran F )
14 f1of1 
 |-  ( F : dom F -1-1-onto-> ran F -> F : dom F -1-1-> ran F )
15 13 14 syl 
 |-  ( F : dom F -1-1-> _V -> F : dom F -1-1-> ran F )
16 15 ad2antrl 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) -> F : dom F -1-1-> ran F )
17 f1linds 
 |-  ( ( W e. LMod /\ ran F e. ( LIndS ` W ) /\ F : dom F -1-1-> ran F ) -> F LIndF W )
18 11 12 16 17 syl3anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) -> F LIndF W )
19 10 18 impbida 
 |-  ( ( W e. LMod /\ L e. NzRing ) -> ( F LIndF W <-> ( F : dom F -1-1-> _V /\ ran F e. ( LIndS ` W ) ) ) )