Metamath Proof Explorer

Theorem rgmoddim

Description: The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 rgmoddim.1 
 |-  V = ( ringLMod ` F )
2 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
3 2 simplbi 
 |-  ( F e. Field -> F e. DivRing )
4 eqid 
 |-  ( Base ` F ) = ( Base ` F )
5 4 ressid 
 |-  ( F e. Field -> ( F |`s ( Base ` F ) ) = F )
6 5 3 eqeltrd 
 |-  ( F e. Field -> ( F |`s ( Base ` F ) ) e. DivRing )
7 drngring 
 |-  ( F e. DivRing -> F e. Ring )
8 4 subrgid 
 |-  ( F e. Ring -> ( Base ` F ) e. ( SubRing ` F ) )
9 3 7 8 3syl 
 |-  ( F e. Field -> ( Base ` F ) e. ( SubRing ` F ) )
10 rlmval 
 |-  ( ringLMod ` F ) = ( ( subringAlg ` F ) ` ( Base ` F ) )
11 1 10 eqtri 
 |-  V = ( ( subringAlg ` F ) ` ( Base ` F ) )
12 eqid 
 |-  ( F |`s ( Base ` F ) ) = ( F |`s ( Base ` F ) )
13 11 12 sralvec 
 |-  ( ( F e. DivRing /\ ( F |`s ( Base ` F ) ) e. DivRing /\ ( Base ` F ) e. ( SubRing ` F ) ) -> V e. LVec )
14 3 6 9 13 syl3anc 
 |-  ( F e. Field -> V e. LVec )
15 3 7 syl 
 |-  ( F e. Field -> F e. Ring )
16 ssidd 
 |-  ( F e. Field -> ( Base ` F ) C_ ( Base ` F ) )
17 11 4 sraring 
 |-  ( ( F e. Ring /\ ( Base ` F ) C_ ( Base ` F ) ) -> V e. Ring )
18 15 16 17 syl2anc 
 |-  ( F e. Field -> V e. Ring )
19 eqid 
 |-  ( Base ` V ) = ( Base ` V )
20 eqid 
 |-  ( 1r ` V ) = ( 1r ` V )
21 19 20 ringidcl 
 |-  ( V e. Ring -> ( 1r ` V ) e. ( Base ` V ) )
22 18 21 syl 
 |-  ( F e. Field -> ( 1r ` V ) e. ( Base ` V ) )
23 11 4 sradrng 
 |-  ( ( F e. DivRing /\ ( Base ` F ) C_ ( Base ` F ) ) -> V e. DivRing )
24 3 16 23 syl2anc 
 |-  ( F e. Field -> V e. DivRing )
25 eqid 
 |-  ( 0g ` V ) = ( 0g ` V )
26 25 20 drngunz 
 |-  ( V e. DivRing -> ( 1r ` V ) =/= ( 0g ` V ) )
27 24 26 syl 
 |-  ( F e. Field -> ( 1r ` V ) =/= ( 0g ` V ) )
28 19 25 lindssn 
 |-  ( ( V e. LVec /\ ( 1r ` V ) e. ( Base ` V ) /\ ( 1r ` V ) =/= ( 0g ` V ) ) -> { ( 1r ` V ) } e. ( LIndS ` V ) )
29 14 22 27 28 syl3anc 
 |-  ( F e. Field -> { ( 1r ` V ) } e. ( LIndS ` V ) )
30 rspval 
 |-  ( RSpan ` F ) = ( LSpan ` ( ringLMod ` F ) )
31 1 fveq2i 
 |-  ( LSpan ` V ) = ( LSpan ` ( ringLMod ` F ) )
32 30 31 eqtr4i 
 |-  ( RSpan ` F ) = ( LSpan ` V )
33 32 fveq1i 
 |-  ( ( RSpan ` F ) ` { ( 1r ` F ) } ) = ( ( LSpan ` V ) ` { ( 1r ` F ) } )
34 eqid 
 |-  ( RSpan ` F ) = ( RSpan ` F )
35 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
36 34 4 35 rsp1 
 |-  ( F e. Ring -> ( ( RSpan ` F ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
37 33 36 eqtr3id 
 |-  ( F e. Ring -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
38 3 7 37 3syl 
 |-  ( F e. Field -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
39 11 a1i 
 |-  ( F e. Field -> V = ( ( subringAlg ` F ) ` ( Base ` F ) ) )
40 eqidd 
 |-  ( F e. Field -> ( 1r ` F ) = ( 1r ` F ) )
41 39 40 16 sra1r 
 |-  ( F e. Field -> ( 1r ` F ) = ( 1r ` V ) )
42 41 sneqd 
 |-  ( F e. Field -> { ( 1r ` F ) } = { ( 1r ` V ) } )
43 42 fveq2d 
 |-  ( F e. Field -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( ( LSpan ` V ) ` { ( 1r ` V ) } ) )
44 39 16 srabase 
 |-  ( F e. Field -> ( Base ` F ) = ( Base ` V ) )
45 38 43 44 3eqtr3d 
 |-  ( F e. Field -> ( ( LSpan ` V ) ` { ( 1r ` V ) } ) = ( Base ` V ) )
46 eqid 
 |-  ( LBasis ` V ) = ( LBasis ` V )
47 eqid 
 |-  ( LSpan ` V ) = ( LSpan ` V )
48 19 46 47 islbs4 
 |-  ( { ( 1r ` V ) } e. ( LBasis ` V ) <-> ( { ( 1r ` V ) } e. ( LIndS ` V ) /\ ( ( LSpan ` V ) ` { ( 1r ` V ) } ) = ( Base ` V ) ) )
49 29 45 48 sylanbrc 
 |-  ( F e. Field -> { ( 1r ` V ) } e. ( LBasis ` V ) )
50 46 dimval 
 |-  ( ( V e. LVec /\ { ( 1r ` V ) } e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` { ( 1r ` V ) } ) )
51 14 49 50 syl2anc 
 |-  ( F e. Field -> ( dim ` V ) = ( # ` { ( 1r ` V ) } ) )
52 fvex 
 |-  ( 1r ` V ) e. _V
53 hashsng 
 |-  ( ( 1r ` V ) e. _V -> ( # ` { ( 1r ` V ) } ) = 1 )
54 52 53 ax-mp 
 |-  ( # ` { ( 1r ` V ) } ) = 1
55 51 54 eqtrdi 
 |-  ( F e. Field -> ( dim ` V ) = 1 )