Metamath Proof Explorer

Theorem lindff1

Description: A linearly independent family over a nonzero ring has no repeated elements. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses lindff1.b 
|- B = ( Base ` W )
lindff1.l 
|- L = ( Scalar ` W )
Assertion lindff1 
|- ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> F : dom F -1-1-> B )

Proof

Step Hyp Ref Expression
1 lindff1.b 
 |-  B = ( Base ` W )
2 lindff1.l 
 |-  L = ( Scalar ` W )
3 simp3 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> F LIndF W )
4 simp1 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> W e. LMod )
5 1 lindff 
 |-  ( ( F LIndF W /\ W e. LMod ) -> F : dom F --> B )
6 3 4 5 syl2anc 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> F : dom F --> B )
7 simpl1 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> W e. LMod )
8 imassrn 
 |-  ( F " ( dom F \ { y } ) ) C_ ran F
9 6 frnd 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> ran F C_ B )
10 8 9 sstrid 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> ( F " ( dom F \ { y } ) ) C_ B )
11 10 adantr 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> ( F " ( dom F \ { y } ) ) C_ B )
12 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
13 1 12 lspssid 
 |-  ( ( W e. LMod /\ ( F " ( dom F \ { y } ) ) C_ B ) -> ( F " ( dom F \ { y } ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
14 7 11 13 syl2anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> ( F " ( dom F \ { y } ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
15 6 ffund 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> Fun F )
16 15 adantr 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> Fun F )
17 simprll 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> x e. dom F )
18 16 17 jca 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> ( Fun F /\ x e. dom F ) )
19 eldifsn 
 |-  ( x e. ( dom F \ { y } ) <-> ( x e. dom F /\ x =/= y ) )
20 19 biimpri 
 |-  ( ( x e. dom F /\ x =/= y ) -> x e. ( dom F \ { y } ) )
21 20 adantlr 
 |-  ( ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) -> x e. ( dom F \ { y } ) )
22 21 adantl 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> x e. ( dom F \ { y } ) )
23 funfvima 
 |-  ( ( Fun F /\ x e. dom F ) -> ( x e. ( dom F \ { y } ) -> ( F ` x ) e. ( F " ( dom F \ { y } ) ) ) )
24 18 22 23 sylc 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> ( F ` x ) e. ( F " ( dom F \ { y } ) ) )
25 14 24 sseldd 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> ( F ` x ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
26 simpl2 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> L e. NzRing )
27 simpl3 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> F LIndF W )
28 simprlr 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> y e. dom F )
29 12 2 lindfind2 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ y e. dom F ) -> -. ( F ` y ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
30 7 26 27 28 29 syl211anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> -. ( F ` y ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) )
31 nelne2 
 |-  ( ( ( F ` x ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) /\ -. ( F ` y ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { y } ) ) ) ) -> ( F ` x ) =/= ( F ` y ) )
32 25 30 31 syl2anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( ( x e. dom F /\ y e. dom F ) /\ x =/= y ) ) -> ( F ` x ) =/= ( F ` y ) )
33 32 expr 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( x e. dom F /\ y e. dom F ) ) -> ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) )
34 33 necon4d 
 |-  ( ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
35 34 ralrimivva 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> A. x e. dom F A. y e. dom F ( ( F ` x ) = ( F ` y ) -> x = y ) )
36 dff13 
 |-  ( F : dom F -1-1-> B <-> ( F : dom F --> B /\ A. x e. dom F A. y e. dom F ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
37 6 35 36 sylanbrc 
 |-  ( ( W e. LMod /\ L e. NzRing /\ F LIndF W ) -> F : dom F -1-1-> B )