Metamath Proof Explorer

Theorem uvcf1

Description: In a nonzero ring, each unit vector is different. (Contributed by Stefan O'Rear, 7-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses uvcff.u 
|- U = ( R unitVec I )
uvcff.y 
|- Y = ( R freeLMod I )
uvcff.b 
|- B = ( Base ` Y )
Assertion uvcf1 
|- ( ( R e. NzRing /\ I e. W ) -> U : I -1-1-> B )

Proof

Step Hyp Ref Expression
1 uvcff.u 
 |-  U = ( R unitVec I )
2 uvcff.y 
 |-  Y = ( R freeLMod I )
3 uvcff.b 
 |-  B = ( Base ` Y )
4 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
5 1 2 3 uvcff 
 |-  ( ( R e. Ring /\ I e. W ) -> U : I --> B )
6 4 5 sylan 
 |-  ( ( R e. NzRing /\ I e. W ) -> U : I --> B )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 7 8 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
10 9 ad3antrrr 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> ( 1r ` R ) =/= ( 0g ` R ) )
11 4 ad3antrrr 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> R e. Ring )
12 simpllr 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> I e. W )
13 simplrl 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> i e. I )
14 1 11 12 13 7 uvcvv1 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> ( ( U ` i ) ` i ) = ( 1r ` R ) )
15 simplrr 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> j e. I )
16 simpr 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> i =/= j )
17 16 necomd 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> j =/= i )
18 1 11 12 15 13 17 8 uvcvv0 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> ( ( U ` j ) ` i ) = ( 0g ` R ) )
19 10 14 18 3netr4d 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> ( ( U ` i ) ` i ) =/= ( ( U ` j ) ` i ) )
20 fveq1 
 |-  ( ( U ` i ) = ( U ` j ) -> ( ( U ` i ) ` i ) = ( ( U ` j ) ` i ) )
21 20 necon3i 
 |-  ( ( ( U ` i ) ` i ) =/= ( ( U ` j ) ` i ) -> ( U ` i ) =/= ( U ` j ) )
22 19 21 syl 
 |-  ( ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) /\ i =/= j ) -> ( U ` i ) =/= ( U ` j ) )
23 22 ex 
 |-  ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) -> ( i =/= j -> ( U ` i ) =/= ( U ` j ) ) )
24 23 necon4d 
 |-  ( ( ( R e. NzRing /\ I e. W ) /\ ( i e. I /\ j e. I ) ) -> ( ( U ` i ) = ( U ` j ) -> i = j ) )
25 24 ralrimivva 
 |-  ( ( R e. NzRing /\ I e. W ) -> A. i e. I A. j e. I ( ( U ` i ) = ( U ` j ) -> i = j ) )
26 dff13 
 |-  ( U : I -1-1-> B <-> ( U : I --> B /\ A. i e. I A. j e. I ( ( U ` i ) = ( U ` j ) -> i = j ) ) )
27 6 25 26 sylanbrc 
 |-  ( ( R e. NzRing /\ I e. W ) -> U : I -1-1-> B )