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 e. DivRing /\ I e. V ) -> ( dim ` F ) = ( # ` I ) )

Proof

Step Hyp Ref Expression
1 frlmdim.f 
 |-  F = ( R freeLMod I )
2 1 frlmlvec 
 |-  ( ( R e. DivRing /\ I e. V ) -> F e. LVec )
3 drngring 
 |-  ( R e. DivRing -> R e. Ring )
4 eqid 
 |-  ( R unitVec I ) = ( R unitVec I )
5 eqid 
 |-  ( LBasis ` F ) = ( LBasis ` F )
6 1 4 5 frlmlbs 
 |-  ( ( R e. Ring /\ I e. V ) -> ran ( R unitVec I ) e. ( LBasis ` F ) )
7 3 6 sylan 
 |-  ( ( R e. DivRing /\ I e. V ) -> ran ( R unitVec I ) e. ( LBasis ` F ) )
8 5 dimval 
 |-  ( ( F e. LVec /\ ran ( R unitVec I ) e. ( LBasis ` F ) ) -> ( dim ` F ) = ( # ` ran ( R unitVec I ) ) )
9 2 7 8 syl2anc 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( dim ` F ) = ( # ` ran ( R unitVec I ) ) )
10 simpr 
 |-  ( ( R e. DivRing /\ I e. V ) -> I e. V )
11 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
12 eqid 
 |-  ( Base ` F ) = ( Base ` F )
13 4 1 12 uvcf1 
 |-  ( ( R e. NzRing /\ I e. V ) -> ( R unitVec I ) : I -1-1-> ( Base ` F ) )
14 11 13 sylan 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( R unitVec I ) : I -1-1-> ( Base ` F ) )
15 hashf1rn 
 |-  ( ( I e. V /\ ( R unitVec I ) : I -1-1-> ( Base ` F ) ) -> ( # ` ( R unitVec I ) ) = ( # ` ran ( R unitVec I ) ) )
16 10 14 15 syl2anc 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( # ` ( R unitVec I ) ) = ( # ` ran ( R unitVec I ) ) )
17 mptexg 
 |-  ( I e. V -> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V )
18 17 ad2antlr 
 |-  ( ( ( R e. DivRing /\ I e. V ) /\ j e. I ) -> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V )
19 18 ralrimiva 
 |-  ( ( R e. DivRing /\ I e. V ) -> A. j e. I ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V )
20 eqid 
 |-  ( j e. I |-> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( j e. I |-> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
21 20 fnmpt 
 |-  ( A. j e. I ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V -> ( j e. I |-> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) Fn I )
22 19 21 syl 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( j e. I |-> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) Fn I )
23 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
24 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
25 4 23 24 uvcfval 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( R unitVec I ) = ( j e. I |-> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
26 25 fneq1d 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( ( R unitVec I ) Fn I <-> ( j e. I |-> ( k e. I |-> if ( k = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) Fn I ) )
27 22 26 mpbird 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( R unitVec I ) Fn I )
28 hashfn 
 |-  ( ( R unitVec I ) Fn I -> ( # ` ( R unitVec I ) ) = ( # ` I ) )
29 27 28 syl 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( # ` ( R unitVec I ) ) = ( # ` I ) )
30 9 16 29 3eqtr2d 
 |-  ( ( R e. DivRing /\ I e. V ) -> ( dim ` F ) = ( # ` I ) )