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=RfreeLModI
Assertion frlmdim ⊢R∈DivRing∧I∈V→dim⁡F=I

Proof

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