Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rlmdim Structured version   Visualization version   GIF version

Theorem rlmdim 33756
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.)
Hypothesis
Ref Expression
rlmdim.1 𝑉 = (ringLMod‘𝐹)
Assertion
Ref Expression
rlmdim (𝐹 ∈ DivRing → (dim‘𝑉) = 1)

Proof of Theorem rlmdim
StepHypRef Expression
1 rlmdim.1 . . . 4 𝑉 = (ringLMod‘𝐹)
2 rlmlvec 21201 . . . 4 (𝐹 ∈ DivRing → (ringLMod‘𝐹) ∈ LVec)
31, 2eqeltrid 2841 . . 3 (𝐹 ∈ DivRing → 𝑉 ∈ LVec)
4 ssid 3945 . . . . . . . 8 (Base‘𝐹) ⊆ (Base‘𝐹)
5 rlmval 21188 . . . . . . . . . 10 (ringLMod‘𝐹) = ((subringAlg ‘𝐹)‘(Base‘𝐹))
61, 5eqtri 2760 . . . . . . . . 9 𝑉 = ((subringAlg ‘𝐹)‘(Base‘𝐹))
7 eqid 2737 . . . . . . . . 9 (Base‘𝐹) = (Base‘𝐹)
86, 7sradrng 33728 . . . . . . . 8 ((𝐹 ∈ DivRing ∧ (Base‘𝐹) ⊆ (Base‘𝐹)) → 𝑉 ∈ DivRing)
94, 8mpan2 692 . . . . . . 7 (𝐹 ∈ DivRing → 𝑉 ∈ DivRing)
109drngringd 20716 . . . . . 6 (𝐹 ∈ DivRing → 𝑉 ∈ Ring)
11 eqid 2737 . . . . . . 7 (Base‘𝑉) = (Base‘𝑉)
12 eqid 2737 . . . . . . 7 (1r𝑉) = (1r𝑉)
1311, 12ringidcl 20248 . . . . . 6 (𝑉 ∈ Ring → (1r𝑉) ∈ (Base‘𝑉))
1410, 13syl 17 . . . . 5 (𝐹 ∈ DivRing → (1r𝑉) ∈ (Base‘𝑉))
15 eqid 2737 . . . . . . 7 (0g𝑉) = (0g𝑉)
1615, 12drngunz 20726 . . . . . 6 (𝑉 ∈ DivRing → (1r𝑉) ≠ (0g𝑉))
179, 16syl 17 . . . . 5 (𝐹 ∈ DivRing → (1r𝑉) ≠ (0g𝑉))
1811, 15lindssn 33440 . . . . 5 ((𝑉 ∈ LVec ∧ (1r𝑉) ∈ (Base‘𝑉) ∧ (1r𝑉) ≠ (0g𝑉)) → {(1r𝑉)} ∈ (LIndS‘𝑉))
193, 14, 17, 18syl3anc 1374 . . . 4 (𝐹 ∈ DivRing → {(1r𝑉)} ∈ (LIndS‘𝑉))
20 drngring 20715 . . . . . 6 (𝐹 ∈ DivRing → 𝐹 ∈ Ring)
211fveq2i 6845 . . . . . . . 8 (LSpan‘𝑉) = (LSpan‘(ringLMod‘𝐹))
22 rspval 21211 . . . . . . . 8 (RSpan‘𝐹) = (LSpan‘(ringLMod‘𝐹))
2321, 22eqtr4i 2763 . . . . . . 7 (LSpan‘𝑉) = (RSpan‘𝐹)
24 eqid 2737 . . . . . . 7 (1r𝐹) = (1r𝐹)
2523, 7, 24rsp1 21237 . . . . . 6 (𝐹 ∈ Ring → ((LSpan‘𝑉)‘{(1r𝐹)}) = (Base‘𝐹))
2620, 25syl 17 . . . . 5 (𝐹 ∈ DivRing → ((LSpan‘𝑉)‘{(1r𝐹)}) = (Base‘𝐹))
276a1i 11 . . . . . . . 8 (𝐹 ∈ DivRing → 𝑉 = ((subringAlg ‘𝐹)‘(Base‘𝐹)))
28 eqidd 2738 . . . . . . . 8 (𝐹 ∈ DivRing → (1r𝐹) = (1r𝐹))
29 ssidd 3946 . . . . . . . 8 (𝐹 ∈ DivRing → (Base‘𝐹) ⊆ (Base‘𝐹))
3027, 28, 29sra1r 33727 . . . . . . 7 (𝐹 ∈ DivRing → (1r𝐹) = (1r𝑉))
3130sneqd 4580 . . . . . 6 (𝐹 ∈ DivRing → {(1r𝐹)} = {(1r𝑉)})
3231fveq2d 6846 . . . . 5 (𝐹 ∈ DivRing → ((LSpan‘𝑉)‘{(1r𝐹)}) = ((LSpan‘𝑉)‘{(1r𝑉)}))
3327, 29srabase 21174 . . . . 5 (𝐹 ∈ DivRing → (Base‘𝐹) = (Base‘𝑉))
3426, 32, 333eqtr3d 2780 . . . 4 (𝐹 ∈ DivRing → ((LSpan‘𝑉)‘{(1r𝑉)}) = (Base‘𝑉))
35 eqid 2737 . . . . 5 (LBasis‘𝑉) = (LBasis‘𝑉)
36 eqid 2737 . . . . 5 (LSpan‘𝑉) = (LSpan‘𝑉)
3711, 35, 36islbs4 21814 . . . 4 ({(1r𝑉)} ∈ (LBasis‘𝑉) ↔ ({(1r𝑉)} ∈ (LIndS‘𝑉) ∧ ((LSpan‘𝑉)‘{(1r𝑉)}) = (Base‘𝑉)))
3819, 34, 37sylanbrc 584 . . 3 (𝐹 ∈ DivRing → {(1r𝑉)} ∈ (LBasis‘𝑉))
3935dimval 33747 . . 3 ((𝑉 ∈ LVec ∧ {(1r𝑉)} ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘{(1r𝑉)}))
403, 38, 39syl2anc 585 . 2 (𝐹 ∈ DivRing → (dim‘𝑉) = (♯‘{(1r𝑉)}))
41 fvex 6855 . . 3 (1r𝑉) ∈ V
42 hashsng 14333 . . 3 ((1r𝑉) ∈ V → (♯‘{(1r𝑉)}) = 1)
4341, 42ax-mp 5 . 2 (♯‘{(1r𝑉)}) = 1
4440, 43eqtrdi 2788 1 (𝐹 ∈ DivRing → (dim‘𝑉) = 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2114  wne 2933  Vcvv 3430  wss 3890  {csn 4568  cfv 6500  1c1 11041  chash 14294  Basecbs 17181  0gc0g 17404  1rcur 20164  Ringcrg 20216  DivRingcdr 20708  LSpanclspn 20968  LBasisclbs 21071  LVecclvec 21099  subringAlg csra 21168  ringLModcrglmod 21169  RSpancrsp 21207  LIndSclinds 21787  dimcldim 33745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7691  ax-reg 9509  ax-inf2 9564  ax-ac2 10387  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7820  df-1st 7944  df-2nd 7945  df-tpos 8178  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-oi 9427  df-r1 9690  df-rank 9691  df-card 9865  df-acn 9868  df-ac 10040  df-pnf 11183  df-mnf 11184  df-xr 11185  df-ltxr 11186  df-le 11187  df-sub 11381  df-neg 11382  df-nn 12177  df-2 12246  df-3 12247  df-4 12248  df-5 12249  df-6 12250  df-7 12251  df-8 12252  df-9 12253  df-n0 12440  df-xnn0 12513  df-z 12527  df-dec 12647  df-uz 12791  df-fz 13464  df-hash 14295  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17182  df-ress 17203  df-plusg 17235  df-mulr 17236  df-sca 17238  df-vsca 17239  df-ip 17240  df-tset 17241  df-ple 17242  df-ocomp 17243  df-0g 17406  df-mre 17550  df-mrc 17551  df-mri 17552  df-acs 17553  df-proset 18262  df-drs 18263  df-poset 18281  df-ipo 18496  df-mgm 18610  df-sgrp 18689  df-mnd 18705  df-submnd 18754  df-grp 18914  df-minusg 18915  df-sbg 18916  df-subg 19101  df-cmn 19759  df-abl 19760  df-mgp 20124  df-rng 20136  df-ur 20165  df-ring 20218  df-oppr 20319  df-dvdsr 20339  df-unit 20340  df-invr 20370  df-subrg 20549  df-drng 20710  df-lmod 20859  df-lss 20929  df-lsp 20969  df-lbs 21072  df-lvec 21100  df-sra 21170  df-rgmod 21171  df-lidl 21208  df-rsp 21209  df-lindf 21788  df-linds 21789  df-dim 33746
This theorem is referenced by:  extdgid  33806
  Copyright terms: Public domain W3C validator