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\mathrm{unitVec}I$$
Assertion	uvcf1o	$$⊢\left(R\in \mathrm{NzRing}\wedge I\in W\right)\to U:I\underset{1-1\; onto}{⟶}\mathrm{ran}U$$

Proof

Step	Hyp	Ref	Expression
1		uvcf1o.u	$$⊢U=R\mathrm{unitVec}I$$
2		eqid	$$⊢R\mathrm{freeLMod}I=R\mathrm{freeLMod}I$$
3		eqid	$$⊢{\mathrm{Base}}_{\left(R\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left(R\mathrm{freeLMod}I\right)}$$
4	1 2 3	uvcf1	$$⊢\left(R\in \mathrm{NzRing}\wedge I\in W\right)\to U:I\underset{1-1}{⟶}{\mathrm{Base}}_{\left(R\mathrm{freeLMod}I\right)}$$
5		f1f1orn	$$⊢U:I\underset{1-1}{⟶}{\mathrm{Base}}_{\left(R\mathrm{freeLMod}I\right)}\to U:I\underset{1-1\; onto}{⟶}\mathrm{ran}U$$
6	4 5	syl	$$⊢\left(R\in \mathrm{NzRing}\wedge I\in W\right)\to U:I\underset{1-1\; onto}{⟶}\mathrm{ran}U$$