MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringidcl Structured version   Visualization version   GIF version

Theorem ringidcl 18788
Description: The unit element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
Hypotheses
Ref Expression
ringidcl.b 𝐵 = (Base‘𝑅)
ringidcl.u 1 = (1r𝑅)
Assertion
Ref Expression
ringidcl (𝑅 ∈ Ring → 1𝐵)

Proof of Theorem ringidcl
StepHypRef Expression
1 eqid 2760 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21ringmgp 18773 . 2 (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3 ringidcl.b . . . 4 𝐵 = (Base‘𝑅)
41, 3mgpbas 18715 . . 3 𝐵 = (Base‘(mulGrp‘𝑅))
5 ringidcl.u . . . 4 1 = (1r𝑅)
61, 5ringidval 18723 . . 3 1 = (0g‘(mulGrp‘𝑅))
74, 6mndidcl 17529 . 2 ((mulGrp‘𝑅) ∈ Mnd → 1𝐵)
82, 7syl 17 1 (𝑅 ∈ Ring → 1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  cfv 6049  Basecbs 16079  Mndcmnd 17515  mulGrpcmgp 18709  1rcur 18721  Ringcrg 18767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-nn 11233  df-2 11291  df-ndx 16082  df-slot 16083  df-base 16085  df-sets 16086  df-plusg 16176  df-0g 16324  df-mgm 17463  df-sgrp 17505  df-mnd 17516  df-mgp 18710  df-ur 18722  df-ring 18769
This theorem is referenced by:  ringid  18794  rngo2times  18796  ringcom  18799  ringnegl  18814  rngnegr  18815  ringmneg1  18816  ringmneg2  18817  imasring  18839  opprring  18851  dvdsrid  18871  dvdsrneg  18874  1unit  18878  ringinvdv  18914  isdrng2  18979  isdrngd  18994  subrgid  19004  abv1z  19054  abvneg  19056  srng1  19081  issrngd  19083  lmod1cl  19112  lmodvsneg  19129  lmodsubvs  19141  lmodsubdi  19142  lmodsubdir  19143  lmodprop2d  19147  rmodislmod  19153  lssvnegcl  19178  prdslmodd  19191  lmodvsinv  19258  islmhm2  19260  lbsind2  19303  lspsneq  19344  lspexch  19351  lidl1el  19440  rsp1  19446  lpi1  19470  isnzr2  19485  isnzr2hash  19486  0ring01eq  19493  fidomndrnglem  19528  asclf  19559  asclghm  19560  asclmul1  19561  asclmul2  19562  asclrhm  19564  rnascl  19565  assamulgscmlem1  19570  psrlmod  19623  psr1cl  19624  mvrf  19646  mplsubrg  19662  mplmon  19685  mplmonmul  19686  mplcoe1  19687  mplind  19724  evlslem1  19737  coe1pwmul  19871  ply1scl0  19882  ply1scl1  19884  ply1idvr1  19885  lply1binomsc  19899  mulgrhm  20068  chrcl  20096  chrid  20097  chrdvds  20098  chrcong  20099  zncyg  20119  zrhpsgnelbas  20162  uvcvvcl2  20349  uvcff  20352  lindfind2  20379  mamumat1cl  20467  mat1bas  20477  matsc  20478  mat0dimid  20496  mat1mhm  20512  dmatid  20523  scmatscmide  20535  scmatscmiddistr  20536  scmatmats  20539  scmatscm  20541  scmatid  20542  scmataddcl  20544  scmatsubcl  20545  scmatmulcl  20546  smatvscl  20552  scmatrhmcl  20556  scmatf1  20559  scmatmhm  20562  mat0scmat  20566  mat1scmat  20567  mdet0pr  20620  mdet1  20629  mdetunilem8  20647  mdetunilem9  20648  mdetuni0  20649  mdetmul  20651  m2detleiblem5  20653  m2detleiblem6  20654  maducoeval2  20668  maduf  20669  madutpos  20670  madugsum  20671  madulid  20673  minmar1marrep  20678  minmar1cl  20679  marep01ma  20688  smadiadetglem1  20699  smadiadetglem2  20700  matinv  20705  1pmatscmul  20729  1elcpmat  20742  mat2pmat1  20759  decpmatid  20797  idpm2idmp  20828  chmatcl  20855  chmatval  20856  chpmat1dlem  20862  chpmat1d  20863  chpdmatlem0  20864  chpdmatlem2  20866  chpdmatlem3  20867  chpidmat  20874  chmaidscmat  20875  cpmidgsumm2pm  20896  cpmidpmatlem2  20898  cpmidpmatlem3  20899  cpmadugsumlemB  20901  cpmadugsumfi  20904  cpmidgsum2  20906  chcoeffeqlem  20912  tlmtgp  22220  nrginvrcnlem  22716  clmvsubval  23129  cvsmuleqdivd  23154  cphsubrglem  23197  deg1pwle  24098  deg1pw  24099  ply1nz  24100  ply1remlem  24141  dchrmulcl  25194  dchrinv  25206  dchrhash  25216  lgsqrlem1  25291  lgsqrlem2  25292  lgsqrlem3  25293  lgsqrlem4  25294  orng0le1  30142  ofldchr  30144  suborng  30145  isarchiofld  30147  elrhmunit  30150  submatminr1  30206  madjusmdetlem1  30223  zrhnm  30343  zrhchr  30350  qqh1  30359  qqhucn  30366  lflsub  34875  eqlkr  34907  eqlkr3  34909  lduallmodlem  34960  ldualvsubcl  34964  ldualvsubval  34965  dochfl1  37285  lcfrlem2  37352  lcdvsubval  37427  mapdpglem30  37511  hgmapval1  37705  hdmapglem5  37734  mendlmod  38283  idomodle  38294  isdomn3  38302  mon1pid  38303  mon1psubm  38304  deg1mhm  38305  lidldomn1  42449  mgpsumn  42670  ascl0  42693  ascl1  42694  ply1sclrmsm  42699  coe1id  42700  evl1at1  42708  linc0scn0  42740  linc1  42742  islindeps2  42800  lmod1lem5  42808
  Copyright terms: Public domain W3C validator