Theorem ringidcl 20500

Description: The unity element of a ring belongs to the base set of the ring. (Contributed by FL, 12-Feb-2010.) (Revised 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 2760	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20471	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringidcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20371	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringidcl.u	. . . 4 ⊢ 1 = (1r‘𝑅)
6	1, 5	ringidval 20415	. . 3 ⊢ 1 = (0g‘(mulGrp‘𝑅))
7	4, 6	mndidcl 18945	. 2 ⊢ ((mulGrp‘𝑅) ∈ Mnd → 1 ∈ 𝐵)
8	2, 7	syl 18	1 ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6539  Basecbs 17393  Mndcmnd 18929  mulGrpcmgp 20366  1_rcur 20413  Ringcrg 20465

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-2 12409  df-sets 17348  df-slot 17366  df-ndx 17378  df-base 17394  df-plusg 17447  df-0g 17618  df-mgm 18822  df-sgrp 18914  df-mnd 18930  df-mgp 20367  df-ur 20414  df-ring 20467

This theorem is used by:  ringidcld  20501  ringid  20509  ringo2times  20510  ringadd2  20511  ringcomlem  20514  ringnegl  20539  ringnegr  20540  ringmneg1  20541  ringmneg2  20542  pwspjmhmmgpd  20563  imasring  20566  xpsring1d  20569  opprring  20583  dvdsrid  20603  dvdsrneg  20606  1unit  20610  ringinvdv  20650  rngisomfv1  20701  rngisom1  20702  rngisomring1  20704  elrhmunit  20766  isnzr2  20774  drnglidl1ne0  20775  isnzr2hash  20776  0ring01eq  20786  subrgid  20831  rrgnz  20962  isdomn3  20972  isdrng2  21003  isdrng3lem1  21011  isdrng3lem2  21012  isdrngd  21028  isdrngdOLD  21030  fidomndrnglem  21036  abv1z  21087  abvneg  21089  srng1  21116  issrngd  21118  orng0le1  21137  suborng  21139  lmod1cl  21170  lmodvsneg  21187  lmodsubvs  21199  lmodsubdi  21200  lmodsubdir  21201  lmodprop2d  21205  rmodislmod  21211  lssvnegcl  21237  prdslmodd  21250  lmodvsinv  21317  islmhm2  21319  lbsind2  21362  lspsneq  21406  lspexch  21413  lidl1el  21511  rsp1  21526  drngidl  21545  rhmqusnsg  21587  rngqiprng1elbas  21588  rngqiprngghmlem1  21589  rngqiprngimf  21599  rngqiprngimf1  21602  rng2idl1cntr  21607  rngqiprngfulem1  21613  rngqiprngfulem4  21616  rngqiprngfulem5  21617  rngqiprngu  21620  rhmpreimaprmidl  21641  qsnzr  21645  ssdifidlprm  21648  prmidlsubm  21649  lpi1  21657  mulgrhm  21789  chrcl  21836  chrid  21837  chrdvds  21838  chrcong  21839  dvdschrmulg  21840  zncyg  21860  frobrhm  21887  ofldchr  21888  zrhpsgnelbas  21906  uvcvvcl2  22100  uvcff  22103  lindfind2  22130  sraassab  22182  asclf  22195  asclghm  22196  ascl0  22198  ascl1  22199  asclmul1  22200  asclmul2  22201  rnascl  22205  assamulgscmlem1  22213  asclmulg  22216  psrlmod  22273  psr1cl  22274  psrascl  22292  mvrf  22298  mplsubrg  22318  mplmon  22350  mplmonmul  22351  mplcoe1  22352  mplind  22385  evlslem1  22397  evlsmaprhm  22446  mhppwdeg  22477  psd1  22494  psdascl  22495  coe1pwmul  22604  coe1id  22618  ply1chr  22630  lply1binomsc  22635  evls1maprhm  22700  rhmmpl  22704  rhmply1vr1  22708  mamumat1cl  22760  mat1bas  22770  matsc  22771  mat0dimid  22789  mat1mhm  22805  dmatid  22816  scmatscmide  22828  scmatscmiddistr  22829  scmatmats  22832  scmatscm  22834  scmatid  22835  scmataddcl  22837  scmatsubcl  22838  scmatmulcl  22839  smatvscl  22845  scmatrhmcl  22849  scmatf1  22852  scmatmhm  22855  mat0scmat  22859  mat1scmat  22860  mdet0pr  22913  mdet1  22922  mdetunilem8  22940  mdetunilem9  22941  mdetuni0  22942  mdetmul  22944  m2detleiblem5  22946  m2detleiblem6  22947  maducoeval2  22961  maduf  22962  madutpos  22963  madugsum  22964  madulid  22966  minmar1marrep  22971  minmar1cl  22972  marep01ma  22981  smadiadetglem1  22992  smadiadetglem2  22993  matinv  22998  1pmatscmul  23026  1elcpmat  23039  mat2pmat1  23056  decpmatid  23094  idpm2idmp  23125  chmatcl  23152  chmatval  23153  chpmat1dlem  23159  chpmat1d  23160  chpdmatlem0  23161  chpdmatlem2  23163  chpdmatlem3  23164  chpidmat  23171  chmaidscmat  23172  cpmidgsumm2pm  23193  cpmidpmatlem2  23195  cpmidpmatlem3  23196  cpmadugsumlemB  23198  cpmadugsumfi  23201  cpmidgsum2  23203  chcoeffeqlem  23209  tlmtgp  24521  nrginvrcnlem  25016  clmvsubval  25436  cvsmuleqdivd  25461  cphsubrglem  25504  deg1pwle  26444  deg1pw  26445  ply1nz  26446  mon1pid  26478  ply1remlem  26489  dchrmulcl  27582  dchrinv  27594  dchrhash  27604  lgsqrlem1  27679  lgsqrlem2  27680  lgsqrlem3  27681  lgsqrlem4  27682  isarchiofld  33807  elrgspnlem2  33851  fracerl  33915  fracfld  33917  primefldgen1  33930  imaslmod  33961  dvdsruasso  33987  rhmquskerlem  34022  elrspunidl  34025  elrspunsn  34026  drngidlhash  34030  mxidlprm  34042  drng0mxidl  34047  qsdrngilem  34065  qsdrnglem2  34067  rsprprmprmidl  34101  rprmasso2  34105  rprmirredlem  34109  rprmdvdsprod  34113  1arithufdlem4  34126  ressasclcl  34150  coe1mon  34166  deg1vr  34171  psrmon  34228  psrmonmul  34229  rlmdim  34289  drngdimgt0  34297  extdg1id  34345  ply1annnr  34382  rtelextdg2lem  34405  submatminr1  34489  madjusmdetlem1  34506  zarcmplem  34560  zrhnm  34646  zrhchr  34653  zrhcntr  34658  qqh1  34664  qqhucn  34671  lflsub  40218  eqlkr  40250  eqlkr3  40252  lduallmodlem  40303  ldualvsubcl  40307  ldualvsubval  40308  dochfl1  42627  lcfrlem2  42694  lcdvsubval  42769  mapdpglem30  42853  hgmapval1  43044  hdmapglem5  43073  rhmzrhval  43116  aks6d1c1p6  43258  deg1gprod  43284  deg1pow  43285  aks5lem2  43331  unitscyglem5  43343  rnasclg  43657  ricdrng1  43686  fidomncyc  43693  rhmpsr  43705  evlsbagval  43708  0prjspnrel  43757  mendlmod  44285  idomodle  44287  mon1psubm  44295  deg1mhm  44296  lidldomn1  49422  smprngprmrng  49530  isidom3  49536  mgpsumn  49569  ply1sclrmsm  49590  evl1at1  49598  linc0scn0  49629  linc1  49631  islindeps2  49689  lmod1lem5  49697  asclelbasALT  50214