Theorem ringidcl 20168

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

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20142	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringidcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20048	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringidcl.u	. . . 4 ⊢ 1 = (1r‘𝑅)
6	1, 5	ringidval 20086	. . 3 ⊢ 1 = (0g‘(mulGrp‘𝑅))
7	4, 6	mndidcl 18641	. 2 ⊢ ((mulGrp‘𝑅) ∈ Mnd → 1 ∈ 𝐵)
8	2, 7	syl 17	1 ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  Basecbs 17138  Mndcmnd 18626  mulGrpcmgp 20043  1_rcur 20084  Ringcrg 20136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-nn 12147  df-2 12209  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17139  df-plusg 17192  df-0g 17363  df-mgm 18532  df-sgrp 18611  df-mnd 18627  df-mgp 20044  df-ur 20085  df-ring 20138

This theorem is referenced by:  ringidcld  20169  ringid  20177  ringo2times  20178  ringadd2  20179  ringcomlem  20182  ringnegl  20205  ringnegr  20206  ringmneg1  20207  ringmneg2  20208  pwspjmhmmgpd  20231  imasring  20233  xpsring1d  20236  opprring  20250  dvdsrid  20270  dvdsrneg  20273  1unit  20277  ringinvdv  20317  rngisomfv1  20368  rngisom1  20369  rngisomring1  20371  elrhmunit  20413  isnzr2  20421  isnzr2hash  20422  0ring01eq  20432  subrgid  20476  rrgnz  20607  isdomn3  20618  isdrng2  20646  isdrngd  20668  isdrngdOLD  20670  fidomndrnglem  20675  abv1z  20727  abvneg  20729  srng1  20756  issrngd  20758  orng0le1  20777  suborng  20779  lmod1cl  20810  lmodvsneg  20827  lmodsubvs  20839  lmodsubdi  20840  lmodsubdir  20841  lmodprop2d  20845  rmodislmod  20851  lssvnegcl  20877  prdslmodd  20890  lmodvsinv  20958  islmhm2  20960  lbsind2  21003  lspsneq  21047  lspexch  21054  lidl1el  21151  rsp1  21162  rhmqusnsg  21210  rngqiprng1elbas  21211  rngqiprngghmlem1  21212  rngqiprngimf  21222  rngqiprngimf1  21225  rng2idl1cntr  21230  rngqiprngfulem1  21236  rngqiprngfulem4  21239  rngqiprngfulem5  21240  rngqiprngu  21243  lpi1  21252  mulgrhm  21402  chrcl  21449  chrid  21450  chrdvds  21451  chrcong  21452  dvdschrmulg  21453  zncyg  21473  frobrhm  21500  ofldchr  21501  zrhpsgnelbas  21519  uvcvvcl2  21713  uvcff  21716  lindfind2  21743  sraassab  21793  asclf  21807  asclghm  21808  ascl0  21809  ascl1  21810  asclmul1  21811  asclmul2  21812  ascldimul  21813  rnascl  21816  assamulgscmlem1  21824  asclmulg  21827  psrlmod  21885  psr1cl  21886  psrascl  21904  mvrf  21910  mplsubrg  21930  mplmon  21958  mplmonmul  21959  mplcoe1  21960  mplind  21993  evlslem1  22005  mhppwdeg  22053  psd1  22070  psdascl  22071  coe1pwmul  22181  ply1scl0OLD  22193  ply1scl1OLD  22196  ply1idvr1OLD  22198  ply1chr  22209  lply1binomsc  22214  evls1maprhm  22279  rhmmpl  22286  rhmply1vr1  22290  mamumat1cl  22342  mat1bas  22352  matsc  22353  mat0dimid  22371  mat1mhm  22387  dmatid  22398  scmatscmide  22410  scmatscmiddistr  22411  scmatmats  22414  scmatscm  22416  scmatid  22417  scmataddcl  22419  scmatsubcl  22420  scmatmulcl  22421  smatvscl  22427  scmatrhmcl  22431  scmatf1  22434  scmatmhm  22437  mat0scmat  22441  mat1scmat  22442  mdet0pr  22495  mdet1  22504  mdetunilem8  22522  mdetunilem9  22523  mdetuni0  22524  mdetmul  22526  m2detleiblem5  22528  m2detleiblem6  22529  maducoeval2  22543  maduf  22544  madutpos  22545  madugsum  22546  madulid  22548  minmar1marrep  22553  minmar1cl  22554  marep01ma  22563  smadiadetglem1  22574  smadiadetglem2  22575  matinv  22580  1pmatscmul  22605  1elcpmat  22618  mat2pmat1  22635  decpmatid  22673  idpm2idmp  22704  chmatcl  22731  chmatval  22732  chpmat1dlem  22738  chpmat1d  22739  chpdmatlem0  22740  chpdmatlem2  22742  chpdmatlem3  22743  chpidmat  22750  chmaidscmat  22751  cpmidgsumm2pm  22772  cpmidpmatlem2  22774  cpmidpmatlem3  22775  cpmadugsumlemB  22777  cpmadugsumfi  22780  cpmidgsum2  22782  chcoeffeqlem  22788  tlmtgp  24099  nrginvrcnlem  24595  clmvsubval  25025  cvsmuleqdivd  25050  cphsubrglem  25093  deg1pwle  26041  deg1pw  26042  ply1nz  26043  mon1pid  26075  ply1remlem  26086  dchrmulcl  27176  dchrinv  27188  dchrhash  27198  lgsqrlem1  27273  lgsqrlem2  27274  lgsqrlem3  27275  lgsqrlem4  27276  isarchiofld  33154  elrgspnlem2  33196  fracerl  33258  fracfld  33260  primefldgen1  33273  imaslmod  33303  dvdsruasso  33335  rhmquskerlem  33375  elrspunidl  33378  elrspunsn  33379  drngidl  33383  drngidlhash  33384  rhmpreimaprmidl  33401  qsnzr  33405  ssdifidlprm  33408  mxidlprm  33420  mxidlirredi  33421  drnglidl1ne0  33425  drng0mxidl  33426  qsdrngilem  33444  qsdrnglem2  33446  rsprprmprmidl  33472  rprmasso2  33476  rprmirredlem  33480  rprmdvdsprod  33484  1arithufdlem4  33497  ressasclcl  33519  coe1mon  33533  deg1vr  33537  rlmdim  33584  rgmoddimOLD  33585  drngdimgt0  33593  extdg1id  33640  ply1annnr  33672  rtelextdg2lem  33695  submatminr1  33779  madjusmdetlem1  33796  zarcmplem  33850  zrhnm  33936  zrhchr  33943  zrhcntr  33948  qqh1  33954  qqhucn  33961  lflsub  39048  eqlkr  39080  eqlkr3  39082  lduallmodlem  39133  ldualvsubcl  39137  ldualvsubval  39138  dochfl1  41458  lcfrlem2  41525  lcdvsubval  41600  mapdpglem30  41684  hgmapval1  41875  hdmapglem5  41904  rhmzrhval  41947  aks6d1c1p6  42090  deg1gprod  42116  deg1pow  42117  aks5lem2  42163  unitscyglem5  42175  rnasclg  42475  ricdrng1  42504  fidomncyc  42511  rhmpsr  42528  evlsbagval  42542  evlsmaprhm  42546  0prjspnrel  42603  mendlmod  43165  idomodle  43167  mon1psubm  43175  deg1mhm  43176  lidldomn1  48219  mgpsumn  48351  ply1sclrmsm  48372  coe1id  48373  evl1at1  48381  linc0scn0  48412  linc1  48414  islindeps2  48472  lmod1lem5  48480  asclelbasALT  48995