Theorem ringidcl 20262

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 2737	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20236	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringidcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20142	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringidcl.u	. . . 4 ⊢ 1 = (1r‘𝑅)
6	1, 5	ringidval 20180	. . 3 ⊢ 1 = (0g‘(mulGrp‘𝑅))
7	4, 6	mndidcl 18762	. 2 ⊢ ((mulGrp‘𝑅) ∈ Mnd → 1 ∈ 𝐵)
8	2, 7	syl 17	1 ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  Basecbs 17247  Mndcmnd 18747  mulGrpcmgp 20137  1_rcur 20178  Ringcrg 20230

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-plusg 17310  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mgp 20138  df-ur 20179  df-ring 20232

This theorem is referenced by:  ringidcld  20263  ringid  20271  ringo2times  20272  ringadd2  20273  ringcomlem  20276  ringnegl  20299  ringnegr  20300  ringmneg1  20301  ringmneg2  20302  pwspjmhmmgpd  20325  imasring  20327  xpsring1d  20330  opprring  20347  dvdsrid  20367  dvdsrneg  20370  1unit  20374  ringinvdv  20414  rngisomfv1  20465  rngisom1  20466  rngisomring1  20468  elrhmunit  20510  isnzr2  20518  isnzr2hash  20519  0ring01eq  20529  subrgid  20573  rrgnz  20704  isdomn3  20715  isdrng2  20743  isdrngd  20765  isdrngdOLD  20767  fidomndrnglem  20773  abv1z  20825  abvneg  20827  srng1  20854  issrngd  20856  lmod1cl  20887  lmodvsneg  20904  lmodsubvs  20916  lmodsubdi  20917  lmodsubdir  20918  lmodprop2d  20922  rmodislmod  20928  lssvnegcl  20954  prdslmodd  20967  lmodvsinv  21035  islmhm2  21037  lbsind2  21080  lspsneq  21124  lspexch  21131  lidl1el  21236  rsp1  21247  rhmqusnsg  21295  rngqiprng1elbas  21296  rngqiprngghmlem1  21297  rngqiprngimf  21307  rngqiprngimf1  21310  rng2idl1cntr  21315  rngqiprngfulem1  21321  rngqiprngfulem4  21324  rngqiprngfulem5  21325  rngqiprngu  21328  lpi1  21337  mulgrhm  21488  chrcl  21539  chrid  21540  chrdvds  21541  chrcong  21542  dvdschrmulg  21543  zncyg  21567  frobrhm  21594  zrhpsgnelbas  21612  uvcvvcl2  21808  uvcff  21811  lindfind2  21838  sraassab  21888  asclf  21902  asclghm  21903  ascl0  21904  ascl1  21905  asclmul1  21906  asclmul2  21907  ascldimul  21908  rnascl  21911  assamulgscmlem1  21919  asclmulg  21922  psrlmod  21980  psr1cl  21981  psrascl  21999  mvrf  22005  mplsubrg  22025  mplmon  22053  mplmonmul  22054  mplcoe1  22055  mplind  22094  evlslem1  22106  mhppwdeg  22154  psd1  22171  psdascl  22172  coe1pwmul  22282  ply1scl0OLD  22294  ply1scl1OLD  22297  ply1idvr1OLD  22299  ply1chr  22310  lply1binomsc  22315  evls1maprhm  22380  rhmmpl  22387  rhmply1vr1  22391  mamumat1cl  22445  mat1bas  22455  matsc  22456  mat0dimid  22474  mat1mhm  22490  dmatid  22501  scmatscmide  22513  scmatscmiddistr  22514  scmatmats  22517  scmatscm  22519  scmatid  22520  scmataddcl  22522  scmatsubcl  22523  scmatmulcl  22524  smatvscl  22530  scmatrhmcl  22534  scmatf1  22537  scmatmhm  22540  mat0scmat  22544  mat1scmat  22545  mdet0pr  22598  mdet1  22607  mdetunilem8  22625  mdetunilem9  22626  mdetuni0  22627  mdetmul  22629  m2detleiblem5  22631  m2detleiblem6  22632  maducoeval2  22646  maduf  22647  madutpos  22648  madugsum  22649  madulid  22651  minmar1marrep  22656  minmar1cl  22657  marep01ma  22666  smadiadetglem1  22677  smadiadetglem2  22678  matinv  22683  1pmatscmul  22708  1elcpmat  22721  mat2pmat1  22738  decpmatid  22776  idpm2idmp  22807  chmatcl  22834  chmatval  22835  chpmat1dlem  22841  chpmat1d  22842  chpdmatlem0  22843  chpdmatlem2  22845  chpdmatlem3  22846  chpidmat  22853  chmaidscmat  22854  cpmidgsumm2pm  22875  cpmidpmatlem2  22877  cpmidpmatlem3  22878  cpmadugsumlemB  22880  cpmadugsumfi  22883  cpmidgsum2  22885  chcoeffeqlem  22891  tlmtgp  24204  nrginvrcnlem  24712  clmvsubval  25142  cvsmuleqdivd  25167  cphsubrglem  25211  deg1pwle  26159  deg1pw  26160  ply1nz  26161  mon1pid  26193  ply1remlem  26204  dchrmulcl  27293  dchrinv  27305  dchrhash  27315  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  elrgspnlem2  33247  fracerl  33308  fracfld  33310  primefldgen1  33323  orng0le1  33342  ofldchr  33344  suborng  33345  isarchiofld  33347  imaslmod  33381  dvdsruasso  33413  rhmquskerlem  33453  elrspunidl  33456  elrspunsn  33457  drngidl  33461  drngidlhash  33462  rhmpreimaprmidl  33479  qsnzr  33483  ssdifidlprm  33486  mxidlprm  33498  mxidlirredi  33499  drnglidl1ne0  33503  drng0mxidl  33504  qsdrngilem  33522  qsdrnglem2  33524  rsprprmprmidl  33550  rprmasso2  33554  rprmirredlem  33558  rprmdvdsprod  33562  1arithufdlem4  33575  ressasclcl  33596  coe1mon  33610  deg1vr  33614  rlmdim  33660  rgmoddimOLD  33661  drngdimgt0  33669  extdg1id  33716  ply1annnr  33746  rtelextdg2lem  33767  submatminr1  33809  madjusmdetlem1  33826  zarcmplem  33880  zrhnm  33968  zrhchr  33975  zrhcntr  33980  qqh1  33986  qqhucn  33993  lflsub  39068  eqlkr  39100  eqlkr3  39102  lduallmodlem  39153  ldualvsubcl  39157  ldualvsubval  39158  dochfl1  41478  lcfrlem2  41545  lcdvsubval  41620  mapdpglem30  41704  hgmapval1  41895  hdmapglem5  41924  rhmzrhval  41971  aks6d1c1p6  42115  deg1gprod  42141  deg1pow  42142  aks5lem2  42188  unitscyglem5  42200  rnasclg  42509  ricdrng1  42538  fidomncyc  42545  rhmpsr  42562  evlsbagval  42576  evlsmaprhm  42580  0prjspnrel  42637  mendlmod  43201  idomodle  43203  mon1psubm  43211  deg1mhm  43212  lidldomn1  48147  mgpsumn  48279  ply1sclrmsm  48300  coe1id  48301  evl1at1  48309  linc0scn0  48340  linc1  48342  islindeps2  48400  lmod1lem5  48408  asclelbasALT  48896