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	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
Assertion	uvcf1o	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		uvcf1o.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2		eqid	⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 )
3		eqid	⊢ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
4	1 2 3	uvcf1	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 –1-1→ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
5		f1f1orn	⊢ ( 𝑈 : 𝐼 –1-1→ ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) → 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 )
6	4 5	syl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 )