Metamath Proof Explorer

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 \in NzRing \land I \in W) \to U : I \underset{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 \in NzRing \land I \in W) \to U : I \underset{1-1}{⟶} {Base}_{(R freeLMod I)}$
5		f1f1orn	$⊢ U : I \underset{1-1}{⟶} {Base}_{(R freeLMod I)} \to U : I \underset{1-1 onto}{⟶} ran U$
6	4 5	syl	$⊢ (R \in NzRing \land I \in W) \to U : I \underset{1-1 onto}{⟶} ran U$