Metamath Proof Explorer

Theorem uvcendim

Description: In a nonzero ring, the number of unit vectors of a free module corresponds to the dimension of the free module. (Contributed by AV, 10-Mar-2019)

Ref Expression
Hypothesis uvcf1o.u 
|- U = ( R unitVec I )
Assertion uvcendim 
|- ( ( R e. NzRing /\ I e. W ) -> I ~~ ran U )

Proof

Step Hyp Ref Expression
1 uvcf1o.u 
 |-  U = ( R unitVec I )
2 1 ovexi 
 |-  U e. _V
3 2 a1i 
 |-  ( ( R e. NzRing /\ I e. W ) -> U e. _V )
4 1 uvcf1o 
 |-  ( ( R e. NzRing /\ I e. W ) -> U : I -1-1-onto-> ran U )
5 f1oeq1 
 |-  ( U = u -> ( U : I -1-1-onto-> ran U <-> u : I -1-1-onto-> ran U ) )
6 5 eqcoms 
 |-  ( u = U -> ( U : I -1-1-onto-> ran U <-> u : I -1-1-onto-> ran U ) )
7 6 biimpd 
 |-  ( u = U -> ( U : I -1-1-onto-> ran U -> u : I -1-1-onto-> ran U ) )
8 7 a1i 
 |-  ( ( R e. NzRing /\ I e. W ) -> ( u = U -> ( U : I -1-1-onto-> ran U -> u : I -1-1-onto-> ran U ) ) )
9 4 8 syl7 
 |-  ( ( R e. NzRing /\ I e. W ) -> ( u = U -> ( ( R e. NzRing /\ I e. W ) -> u : I -1-1-onto-> ran U ) ) )
10 9 imp 
 |-  ( ( ( R e. NzRing /\ I e. W ) /\ u = U ) -> ( ( R e. NzRing /\ I e. W ) -> u : I -1-1-onto-> ran U ) )
11 3 10 spcimedv 
 |-  ( ( R e. NzRing /\ I e. W ) -> ( ( R e. NzRing /\ I e. W ) -> E. u u : I -1-1-onto-> ran U ) )
12 11 pm2.43i 
 |-  ( ( R e. NzRing /\ I e. W ) -> E. u u : I -1-1-onto-> ran U )
13 bren 
 |-  ( I ~~ ran U <-> E. u u : I -1-1-onto-> ran U )
14 12 13 sylibr 
 |-  ( ( R e. NzRing /\ I e. W ) -> I ~~ ran U )