This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑈 )