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	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
Assertion	uvcendim	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ≈ ran 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		uvcf1o.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2	1	ovexi	⊢ 𝑈 ∈ V
3	2	a1i	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝑈 ∈ V )
4	1	uvcf1o	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 )
5		f1oeq1	⊢ ( 𝑈 = 𝑢 → ( 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 ↔ 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 ) )
6	5	eqcoms	⊢ ( 𝑢 = 𝑈 → ( 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 ↔ 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 ) )
7	6	biimpd	⊢ ( 𝑢 = 𝑈 → ( 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 → 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 ) )
8	7	a1i	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → ( 𝑢 = 𝑈 → ( 𝑈 : 𝐼 –1-1-onto→ ran 𝑈 → 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 ) ) )
9	4 8	syl7	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → ( 𝑢 = 𝑈 → ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 ) ) )
10	9	imp	⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) ∧ 𝑢 = 𝑈 ) → ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 ) )
11	3 10	spcimedv	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → ∃ 𝑢 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 ) )
12	11	pm2.43i	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → ∃ 𝑢 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 )
13		bren	⊢ ( 𝐼 ≈ ran 𝑈 ↔ ∃ 𝑢 𝑢 : 𝐼 –1-1-onto→ ran 𝑈 )
14	12 13	sylibr	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ≈ ran 𝑈 )