Metamath Proof Explorer

Theorem rlmdim

Description: The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023) Generalize to division rings. (Revised by SN, 22-Mar-2025)

Ref Expression
Hypothesis rlmdim.1 
|- V = ( ringLMod ` F )
Assertion rlmdim 
|- ( F e. DivRing -> ( dim ` V ) = 1 )

Proof

Step Hyp Ref Expression
1 rlmdim.1 
 |-  V = ( ringLMod ` F )
2 rlmlvec 
 |-  ( F e. DivRing -> ( ringLMod ` F ) e. LVec )
3 1 2 eqeltrid 
 |-  ( F e. DivRing -> V e. LVec )
4 ssid 
 |-  ( Base ` F ) C_ ( Base ` F )
5 rlmval 
 |-  ( ringLMod ` F ) = ( ( subringAlg ` F ) ` ( Base ` F ) )
6 1 5 eqtri 
 |-  V = ( ( subringAlg ` F ) ` ( Base ` F ) )
7 eqid 
 |-  ( Base ` F ) = ( Base ` F )
8 6 7 sradrng 
 |-  ( ( F e. DivRing /\ ( Base ` F ) C_ ( Base ` F ) ) -> V e. DivRing )
9 4 8 mpan2 
 |-  ( F e. DivRing -> V e. DivRing )
10 9 drngringd 
 |-  ( F e. DivRing -> V e. Ring )
11 eqid 
 |-  ( Base ` V ) = ( Base ` V )
12 eqid 
 |-  ( 1r ` V ) = ( 1r ` V )
13 11 12 ringidcl 
 |-  ( V e. Ring -> ( 1r ` V ) e. ( Base ` V ) )
14 10 13 syl 
 |-  ( F e. DivRing -> ( 1r ` V ) e. ( Base ` V ) )
15 eqid 
 |-  ( 0g ` V ) = ( 0g ` V )
16 15 12 drngunz 
 |-  ( V e. DivRing -> ( 1r ` V ) =/= ( 0g ` V ) )
17 9 16 syl 
 |-  ( F e. DivRing -> ( 1r ` V ) =/= ( 0g ` V ) )
18 11 15 lindssn 
 |-  ( ( V e. LVec /\ ( 1r ` V ) e. ( Base ` V ) /\ ( 1r ` V ) =/= ( 0g ` V ) ) -> { ( 1r ` V ) } e. ( LIndS ` V ) )
19 3 14 17 18 syl3anc 
 |-  ( F e. DivRing -> { ( 1r ` V ) } e. ( LIndS ` V ) )
20 drngring 
 |-  ( F e. DivRing -> F e. Ring )
21 1 fveq2i 
 |-  ( LSpan ` V ) = ( LSpan ` ( ringLMod ` F ) )
22 rspval 
 |-  ( RSpan ` F ) = ( LSpan ` ( ringLMod ` F ) )
23 21 22 eqtr4i 
 |-  ( LSpan ` V ) = ( RSpan ` F )
24 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
25 23 7 24 rsp1 
 |-  ( F e. Ring -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
26 20 25 syl 
 |-  ( F e. DivRing -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
27 6 a1i 
 |-  ( F e. DivRing -> V = ( ( subringAlg ` F ) ` ( Base ` F ) ) )
28 eqidd 
 |-  ( F e. DivRing -> ( 1r ` F ) = ( 1r ` F ) )
29 ssidd 
 |-  ( F e. DivRing -> ( Base ` F ) C_ ( Base ` F ) )
30 27 28 29 sra1r 
 |-  ( F e. DivRing -> ( 1r ` F ) = ( 1r ` V ) )
31 30 sneqd 
 |-  ( F e. DivRing -> { ( 1r ` F ) } = { ( 1r ` V ) } )
32 31 fveq2d 
 |-  ( F e. DivRing -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( ( LSpan ` V ) ` { ( 1r ` V ) } ) )
33 27 29 srabase 
 |-  ( F e. DivRing -> ( Base ` F ) = ( Base ` V ) )
34 26 32 33 3eqtr3d 
 |-  ( F e. DivRing -> ( ( LSpan ` V ) ` { ( 1r ` V ) } ) = ( Base ` V ) )
35 eqid 
 |-  ( LBasis ` V ) = ( LBasis ` V )
36 eqid 
 |-  ( LSpan ` V ) = ( LSpan ` V )
37 11 35 36 islbs4 
 |-  ( { ( 1r ` V ) } e. ( LBasis ` V ) <-> ( { ( 1r ` V ) } e. ( LIndS ` V ) /\ ( ( LSpan ` V ) ` { ( 1r ` V ) } ) = ( Base ` V ) ) )
38 19 34 37 sylanbrc 
 |-  ( F e. DivRing -> { ( 1r ` V ) } e. ( LBasis ` V ) )
39 35 dimval 
 |-  ( ( V e. LVec /\ { ( 1r ` V ) } e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` { ( 1r ` V ) } ) )
40 3 38 39 syl2anc 
 |-  ( F e. DivRing -> ( dim ` V ) = ( # ` { ( 1r ` V ) } ) )
41 fvex 
 |-  ( 1r ` V ) e. _V
42 hashsng 
 |-  ( ( 1r ` V ) e. _V -> ( # ` { ( 1r ` V ) } ) = 1 )
43 41 42 ax-mp 
 |-  ( # ` { ( 1r ` V ) } ) = 1
44 40 43 eqtrdi 
 |-  ( F e. DivRing -> ( dim ` V ) = 1 )