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

Theorem ringidcl 19914
Description: The unity 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 2738 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21ringmgp 19895 . 2 (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3 ringidcl.b . . . 4 𝐵 = (Base‘𝑅)
41, 3mgpbas 19832 . . 3 𝐵 = (Base‘(mulGrp‘𝑅))
5 ringidcl.u . . . 4 1 = (1r𝑅)
61, 5ringidval 19845 . . 3 1 = (0g‘(mulGrp‘𝑅))
74, 6mndidcl 18506 . 2 ((mulGrp‘𝑅) ∈ Mnd → 1𝐵)
82, 7syl 17 1 (𝑅 ∈ Ring → 1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  cfv 6492  Basecbs 17018  Mndcmnd 18491  mulGrpcmgp 19826  1rcur 19843  Ringcrg 19889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-om 7794  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-er 8582  df-en 8818  df-dom 8819  df-sdom 8820  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-nn 12088  df-2 12150  df-sets 16971  df-slot 16989  df-ndx 17001  df-base 17019  df-plusg 17081  df-0g 17258  df-mgm 18432  df-sgrp 18481  df-mnd 18492  df-mgp 19827  df-ur 19844  df-ring 19891
This theorem is referenced by:  ringid  19920  rngo2times  19922  ringcom  19925  ringnegl  19942  rngnegr  19943  ringmneg1  19944  ringmneg2  19945  pwspjmhmmgpd  19967  imasring  19969  opprring  19984  dvdsrid  20004  dvdsrneg  20007  1unit  20011  ringinvdv  20047  elrhmunit  20107  isdrng2  20122  isdrngd  20138  subrgid  20148  abv1z  20215  abvneg  20217  srng1  20242  issrngd  20244  lmod1cl  20273  lmodvsneg  20290  lmodsubvs  20302  lmodsubdi  20303  lmodsubdir  20304  lmodprop2d  20308  rmodislmod  20314  rmodislmodOLD  20315  lssvnegcl  20341  prdslmodd  20354  lmodvsinv  20421  islmhm2  20423  lbsind2  20466  lspsneq  20507  lspexch  20514  lidl1el  20612  rsp1  20618  lpi1  20642  isnzr2  20657  isnzr2hash  20658  0ring01eq  20665  fidomndrnglem  20701  mulgrhm  20822  chrcl  20853  chrid  20854  chrdvds  20855  chrcong  20856  zncyg  20879  zrhpsgnelbas  20922  uvcvvcl2  21118  uvcff  21121  lindfind2  21148  asclf  21209  asclghm  21210  ascl0  21211  ascl1  21212  asclmul1  21213  asclmul2  21214  ascldimul  21215  rnascl  21218  assamulgscmlem1  21226  psrlmod  21293  psr1cl  21294  mvrf  21316  mplsubrg  21334  mplmon  21359  mplmonmul  21360  mplcoe1  21361  mplind  21401  evlslem1  21415  mhppwdeg  21463  coe1pwmul  21573  ply1scl0  21584  ply1scl1  21586  ply1idvr1  21587  lply1binomsc  21601  mamumat1cl  21711  mat1bas  21721  matsc  21722  mat0dimid  21740  mat1mhm  21756  dmatid  21767  scmatscmide  21779  scmatscmiddistr  21780  scmatmats  21783  scmatscm  21785  scmatid  21786  scmataddcl  21788  scmatsubcl  21789  scmatmulcl  21790  smatvscl  21796  scmatrhmcl  21800  scmatf1  21803  scmatmhm  21806  mat0scmat  21810  mat1scmat  21811  mdet0pr  21864  mdet1  21873  mdetunilem8  21891  mdetunilem9  21892  mdetuni0  21893  mdetmul  21895  m2detleiblem5  21897  m2detleiblem6  21898  maducoeval2  21912  maduf  21913  madutpos  21914  madugsum  21915  madulid  21917  minmar1marrep  21922  minmar1cl  21923  marep01ma  21932  smadiadetglem1  21943  smadiadetglem2  21944  matinv  21949  1pmatscmul  21974  1elcpmat  21987  mat2pmat1  22004  decpmatid  22042  idpm2idmp  22073  chmatcl  22100  chmatval  22101  chpmat1dlem  22107  chpmat1d  22108  chpdmatlem0  22109  chpdmatlem2  22111  chpdmatlem3  22112  chpidmat  22119  chmaidscmat  22120  cpmidgsumm2pm  22141  cpmidpmatlem2  22143  cpmidpmatlem3  22144  cpmadugsumlemB  22146  cpmadugsumfi  22149  cpmidgsum2  22151  chcoeffeqlem  22157  tlmtgp  23470  nrginvrcnlem  23978  clmvsubval  24395  cvsmuleqdivd  24420  cphsubrglem  24464  deg1pwle  25407  deg1pw  25408  ply1nz  25409  ply1remlem  25450  dchrmulcl  26520  dchrinv  26532  dchrhash  26542  lgsqrlem1  26617  lgsqrlem2  26618  lgsqrlem3  26619  lgsqrlem4  26620  dvdschrmulg  31860  frobrhm  31862  primefldgen1  31882  orng0le1  31901  ofldchr  31903  suborng  31904  isarchiofld  31906  imaslmod  31939  elrspunidl  31993  rhmpreimaprmidl  32014  mxidlprm  32027  asclmulg  32053  ply1chr  32066  rgmoddim  32091  drngdimgt0  32099  extdg1id  32136  submatminr1  32165  madjusmdetlem1  32182  zarcmplem  32236  zrhnm  32324  zrhchr  32331  qqh1  32340  qqhucn  32347  lflsub  37425  eqlkr  37457  eqlkr3  37459  lduallmodlem  37510  ldualvsubcl  37514  ldualvsubval  37515  dochfl1  39835  lcfrlem2  39902  lcdvsubval  39977  mapdpglem30  40061  hgmapval1  40252  hdmapglem5  40281  rnasclg  40568  evlsbagval  40630  mhphf  40640  0prjspnrel  40831  mendlmod  41386  idomodle  41389  isdomn3  41397  mon1pid  41398  mon1psubm  41399  deg1mhm  41400  lidldomn1  45969  mgpsumn  46189  ply1sclrmsm  46214  coe1id  46215  evl1at1  46223  linc0scn0  46254  linc1  46256  islindeps2  46314  lmod1lem5  46322
  Copyright terms: Public domain W3C validator