Metamath Proof Explorer

Theorem frlmdim

Description: Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypothesis frlmdim.f ⊢ F = R freeLMod I
Assertion frlmdim ⊢ R ∈ DivRing ∧ I ∈ V → dim ⁡ F = I

Proof

Step Hyp Ref Expression
1 frlmdim.f ⊢ F = R freeLMod I
2 1 frlmlvec ⊢ R ∈ DivRing ∧ I ∈ V → F ∈ LVec
3 drngring ⊢ R ∈ DivRing → R ∈ Ring
4 eqid ⊢ R unitVec I = R unitVec I
5 eqid ⊢ LBasis ⁡ F = LBasis ⁡ F
6 1 4 5 frlmlbs ⊢ R ∈ Ring ∧ I ∈ V → ran ⁡ R unitVec I ∈ LBasis ⁡ F
7 3 6 sylan ⊢ R ∈ DivRing ∧ I ∈ V → ran ⁡ R unitVec I ∈ LBasis ⁡ F
8 5 dimval ⊢ F ∈ LVec ∧ ran ⁡ R unitVec I ∈ LBasis ⁡ F → dim ⁡ F = ran ⁡ R unitVec I
9 2 7 8 syl2anc ⊢ R ∈ DivRing ∧ I ∈ V → dim ⁡ F = ran ⁡ R unitVec I
10 simpr ⊢ R ∈ DivRing ∧ I ∈ V → I ∈ V
11 drngnzr ⊢ R ∈ DivRing → R ∈ NzRing
12 eqid ⊢ Base F = Base F
13 4 1 12 uvcf1 ⊢ R ∈ NzRing ∧ I ∈ V → R unitVec I : I ⟶ 1-1 Base F
14 11 13 sylan ⊢ R ∈ DivRing ∧ I ∈ V → R unitVec I : I ⟶ 1-1 Base F
15 hashf1rn ⊢ I ∈ V ∧ R unitVec I : I ⟶ 1-1 Base F → R unitVec I = ran ⁡ R unitVec I
16 10 14 15 syl2anc ⊢ R ∈ DivRing ∧ I ∈ V → R unitVec I = ran ⁡ R unitVec I
17 mptexg ⊢ I ∈ V → k ∈ I ⟼ if k = j 1 R 0 R ∈ V
18 17 ad2antlr ⊢ R ∈ DivRing ∧ I ∈ V ∧ j ∈ I → k ∈ I ⟼ if k = j 1 R 0 R ∈ V
19 18 ralrimiva ⊢ R ∈ DivRing ∧ I ∈ V → ∀ j ∈ I k ∈ I ⟼ if k = j 1 R 0 R ∈ V
20 eqid ⊢ j ∈ I ⟼ k ∈ I ⟼ if k = j 1 R 0 R = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 R 0 R
21 20 fnmpt ⊢ ∀ j ∈ I k ∈ I ⟼ if k = j 1 R 0 R ∈ V → j ∈ I ⟼ k ∈ I ⟼ if k = j 1 R 0 R Fn I
22 19 21 syl ⊢ R ∈ DivRing ∧ I ∈ V → j ∈ I ⟼ k ∈ I ⟼ if k = j 1 R 0 R Fn I
23 eqid ⊢ 1 R = 1 R
24 eqid ⊢ 0 R = 0 R
25 4 23 24 uvcfval ⊢ R ∈ DivRing ∧ I ∈ V → R unitVec I = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 R 0 R
26 25 fneq1d ⊢ R ∈ DivRing ∧ I ∈ V → R unitVec I Fn I ↔ j ∈ I ⟼ k ∈ I ⟼ if k = j 1 R 0 R Fn I
27 22 26 mpbird ⊢ R ∈ DivRing ∧ I ∈ V → R unitVec I Fn I
28 hashfn ⊢ R unitVec I Fn I → R unitVec I = I
29 27 28 syl ⊢ R ∈ DivRing ∧ I ∈ V → R unitVec I = I
30 9 16 29 3eqtr2d ⊢ R ∈ DivRing ∧ I ∈ V → dim ⁡ F = I