Theorem uvcf1o

Description: In a nonzero ring, the mapping of the index set of a free module onto the unit vectors of the free module is a 1-1 onto function. (Contributed by AV, 10-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		uvcf1o.u	|- U = ( R unitVec I )
2		eqid	|- ( R freeLMod I ) = ( R freeLMod I )
3		eqid	|- ( Base ` ( R freeLMod I ) ) = ( Base ` ( R freeLMod I ) )
4	1 2 3	uvcf1	|- ( ( R e. NzRing /\ I e. W ) -> U : I -1-1-> ( Base ` ( R freeLMod I ) ) )
5		f1f1orn	|- ( U : I -1-1-> ( Base ` ( R freeLMod I ) ) -> U : I -1-1-onto-> ran U )
6	4 5	syl	|- ( ( R e. NzRing /\ I e. W ) -> U : I -1-1-onto-> ran U )