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

Theorem ringidcl 18489
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 2621 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21ringmgp 18474 . 2 (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3 ringidcl.b . . . 4 𝐵 = (Base‘𝑅)
41, 3mgpbas 18416 . . 3 𝐵 = (Base‘(mulGrp‘𝑅))
5 ringidcl.u . . . 4 1 = (1r𝑅)
61, 5ringidval 18424 . . 3 1 = (0g‘(mulGrp‘𝑅))
74, 6mndidcl 17229 . 2 ((mulGrp‘𝑅) ∈ Mnd → 1𝐵)
82, 7syl 17 1 (𝑅 ∈ Ring → 1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  cfv 5847  Basecbs 15781  Mndcmnd 17215  mulGrpcmgp 18410  1rcur 18422  Ringcrg 18468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-plusg 15875  df-0g 16023  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-mgp 18411  df-ur 18423  df-ring 18470
This theorem is referenced by:  ringid  18495  rngo2times  18497  ringcom  18500  ringnegl  18515  rngnegr  18516  ringmneg1  18517  ringmneg2  18518  imasring  18540  opprring  18552  dvdsrid  18572  dvdsrneg  18575  1unit  18579  ringinvdv  18615  isdrng2  18678  isdrngd  18693  subrgid  18703  abv1z  18753  abvneg  18755  srng1  18780  issrngd  18782  lmod1cl  18811  lmodvsneg  18828  lmodsubvs  18840  lmodsubdi  18841  lmodsubdir  18842  lmodprop2d  18846  lssvnegcl  18875  prdslmodd  18888  lmodvsinv  18955  islmhm2  18957  lbsind2  19000  lspsneq  19041  lspexch  19048  lidl1el  19137  rsp1  19143  lpi1  19167  isnzr2  19182  isnzr2hash  19183  0ring01eq  19190  fidomndrnglem  19225  asclf  19256  asclghm  19257  asclmul1  19258  asclmul2  19259  asclrhm  19261  rnascl  19262  assamulgscmlem1  19267  psrlmod  19320  psr1cl  19321  mvrf  19343  mplsubrg  19359  mplmon  19382  mplmonmul  19383  mplcoe1  19384  mplind  19421  evlslem1  19434  coe1pwmul  19568  ply1scl0  19579  ply1scl1  19581  ply1idvr1  19582  lply1binomsc  19596  mulgrhm  19765  chrcl  19793  chrid  19794  chrdvds  19795  chrcong  19796  zncyg  19816  zrhpsgnelbas  19859  uvcvvcl2  20046  uvcff  20049  lindfind2  20076  mamumat1cl  20164  mat1bas  20174  matsc  20175  mat0dimid  20193  mat1mhm  20209  dmatid  20220  scmatscmide  20232  scmatscmiddistr  20233  scmatmats  20236  scmatscm  20238  scmatid  20239  scmataddcl  20241  scmatsubcl  20242  scmatmulcl  20243  smatvscl  20249  scmatrhmcl  20253  scmatf1  20256  scmatmhm  20259  mat0scmat  20263  mat1scmat  20264  mdet0pr  20317  mdet1  20326  mdetunilem8  20344  mdetunilem9  20345  mdetuni0  20346  mdetmul  20348  m2detleiblem5  20350  m2detleiblem6  20351  maducoeval2  20365  maduf  20366  madutpos  20367  madugsum  20368  madulid  20370  minmar1marrep  20375  minmar1cl  20376  marep01ma  20385  smadiadetglem1  20396  smadiadetglem2  20397  matinv  20402  1pmatscmul  20426  1elcpmat  20439  mat2pmat1  20456  decpmatid  20494  idpm2idmp  20525  chmatcl  20552  chmatval  20553  chpmat1dlem  20559  chpmat1d  20560  chpdmatlem0  20561  chpdmatlem2  20563  chpdmatlem3  20564  chpidmat  20571  chmaidscmat  20572  cpmidgsumm2pm  20593  cpmidpmatlem2  20595  cpmidpmatlem3  20596  cpmadugsumlemB  20598  cpmadugsumfi  20601  cpmidgsum2  20603  chcoeffeqlem  20609  tlmtgp  21909  nrginvrcnlem  22405  clmvsubval  22817  cvsmuleqdivd  22842  cphsubrglem  22885  deg1pwle  23783  deg1pw  23784  ply1nz  23785  ply1remlem  23826  dchrmulcl  24874  dchrinv  24886  dchrhash  24896  lgsqrlem1  24971  lgsqrlem2  24972  lgsqrlem3  24973  lgsqrlem4  24974  orng0le1  29597  ofldchr  29599  suborng  29600  isarchiofld  29602  elrhmunit  29605  submatminr1  29658  madjusmdetlem1  29675  zrhnm  29795  zrhchr  29802  qqh1  29811  qqhucn  29818  lflsub  33834  eqlkr  33866  eqlkr3  33868  lduallmodlem  33919  ldualvsubcl  33923  ldualvsubval  33924  dochfl1  36245  lcfrlem2  36312  lcdvsubval  36387  mapdpglem30  36471  hgmapval1  36665  hdmapglem5  36694  mendlmod  37244  idomodle  37255  isdomn3  37263  mon1pid  37264  mon1psubm  37265  deg1mhm  37266  lidldomn1  41209  mgpsumn  41430  ascl0  41453  ascl1  41454  ply1sclrmsm  41459  coe1id  41460  evl1at1  41468  linc0scn0  41500  linc1  41502  islindeps2  41560  lmod1lem5  41568
  Copyright terms: Public domain W3C validator