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 ⊢ U = R unitVec I
Assertion uvcendim ⊢ R ∈ NzRing ∧ I ∈ W → I ≈ ran ⁡ U

Proof

Step Hyp Ref Expression
1 uvcf1o.u ⊢ U = R unitVec I
2 1 ovexi ⊢ U ∈ V
3 2 a1i ⊢ R ∈ NzRing ∧ I ∈ W → U ∈ V
4 1 uvcf1o ⊢ R ∈ NzRing ∧ I ∈ W → U : I ⟶ 1-1 onto ran ⁡ U
5 f1oeq1 ⊢ U = u → U : I ⟶ 1-1 onto ran ⁡ U ↔ u : I ⟶ 1-1 onto ran ⁡ U
6 5 eqcoms ⊢ u = U → U : I ⟶ 1-1 onto ran ⁡ U ↔ u : I ⟶ 1-1 onto ran ⁡ U
7 6 biimpd ⊢ u = U → U : I ⟶ 1-1 onto ran ⁡ U → u : I ⟶ 1-1 onto ran ⁡ U
8 7 a1i ⊢ R ∈ NzRing ∧ I ∈ W → u = U → U : I ⟶ 1-1 onto ran ⁡ U → u : I ⟶ 1-1 onto ran ⁡ U
9 4 8 syl7 ⊢ R ∈ NzRing ∧ I ∈ W → u = U → R ∈ NzRing ∧ I ∈ W → u : I ⟶ 1-1 onto ran ⁡ U
10 9 imp ⊢ R ∈ NzRing ∧ I ∈ W ∧ u = U → R ∈ NzRing ∧ I ∈ W → u : I ⟶ 1-1 onto ran ⁡ U
11 3 10 spcimedv ⊢ R ∈ NzRing ∧ I ∈ W → R ∈ NzRing ∧ I ∈ W → ∃ u u : I ⟶ 1-1 onto ran ⁡ U
12 11 pm2.43i ⊢ R ∈ NzRing ∧ I ∈ W → ∃ u u : I ⟶ 1-1 onto ran ⁡ U
13 bren ⊢ I ≈ ran ⁡ U ↔ ∃ u u : I ⟶ 1-1 onto ran ⁡ U
14 12 13 sylibr ⊢ R ∈ NzRing ∧ I ∈ W → I ≈ ran ⁡ U