Theorem ringidcl 20181

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  Basecbs 17186  Mndcmnd 18668  mulGrpcmgp 20056  1_rcur 20097  Ringcrg 20149

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-2 12256  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-plusg 17240  df-0g 17411  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-mgp 20057  df-ur 20098  df-ring 20151

This theorem is referenced by:  ringidcld  20182  ringid  20190  ringo2times  20191  ringadd2  20192  ringcomlem  20195  ringnegl  20218  ringnegr  20219  ringmneg1  20220  ringmneg2  20221  pwspjmhmmgpd  20244  imasring  20246  xpsring1d  20249  opprring  20263  dvdsrid  20283  dvdsrneg  20286  1unit  20290  ringinvdv  20330  rngisomfv1  20381  rngisom1  20382  rngisomring1  20384  elrhmunit  20426  isnzr2  20434  isnzr2hash  20435  0ring01eq  20445  subrgid  20489  rrgnz  20620  isdomn3  20631  isdrng2  20659  isdrngd  20681  isdrngdOLD  20683  fidomndrnglem  20688  abv1z  20740  abvneg  20742  srng1  20769  issrngd  20771  lmod1cl  20802  lmodvsneg  20819  lmodsubvs  20831  lmodsubdi  20832  lmodsubdir  20833  lmodprop2d  20837  rmodislmod  20843  lssvnegcl  20869  prdslmodd  20882  lmodvsinv  20950  islmhm2  20952  lbsind2  20995  lspsneq  21039  lspexch  21046  lidl1el  21143  rsp1  21154  rhmqusnsg  21202  rngqiprng1elbas  21203  rngqiprngghmlem1  21204  rngqiprngimf  21214  rngqiprngimf1  21217  rng2idl1cntr  21222  rngqiprngfulem1  21228  rngqiprngfulem4  21231  rngqiprngfulem5  21232  rngqiprngu  21235  lpi1  21244  mulgrhm  21394  chrcl  21441  chrid  21442  chrdvds  21443  chrcong  21444  dvdschrmulg  21445  zncyg  21465  frobrhm  21492  zrhpsgnelbas  21510  uvcvvcl2  21704  uvcff  21707  lindfind2  21734  sraassab  21784  asclf  21798  asclghm  21799  ascl0  21800  ascl1  21801  asclmul1  21802  asclmul2  21803  ascldimul  21804  rnascl  21807  assamulgscmlem1  21815  asclmulg  21818  psrlmod  21876  psr1cl  21877  psrascl  21895  mvrf  21901  mplsubrg  21921  mplmon  21949  mplmonmul  21950  mplcoe1  21951  mplind  21984  evlslem1  21996  mhppwdeg  22044  psd1  22061  psdascl  22062  coe1pwmul  22172  ply1scl0OLD  22184  ply1scl1OLD  22187  ply1idvr1OLD  22189  ply1chr  22200  lply1binomsc  22205  evls1maprhm  22270  rhmmpl  22277  rhmply1vr1  22281  mamumat1cl  22333  mat1bas  22343  matsc  22344  mat0dimid  22362  mat1mhm  22378  dmatid  22389  scmatscmide  22401  scmatscmiddistr  22402  scmatmats  22405  scmatscm  22407  scmatid  22408  scmataddcl  22410  scmatsubcl  22411  scmatmulcl  22412  smatvscl  22418  scmatrhmcl  22422  scmatf1  22425  scmatmhm  22428  mat0scmat  22432  mat1scmat  22433  mdet0pr  22486  mdet1  22495  mdetunilem8  22513  mdetunilem9  22514  mdetuni0  22515  mdetmul  22517  m2detleiblem5  22519  m2detleiblem6  22520  maducoeval2  22534  maduf  22535  madutpos  22536  madugsum  22537  madulid  22539  minmar1marrep  22544  minmar1cl  22545  marep01ma  22554  smadiadetglem1  22565  smadiadetglem2  22566  matinv  22571  1pmatscmul  22596  1elcpmat  22609  mat2pmat1  22626  decpmatid  22664  idpm2idmp  22695  chmatcl  22722  chmatval  22723  chpmat1dlem  22729  chpmat1d  22730  chpdmatlem0  22731  chpdmatlem2  22733  chpdmatlem3  22734  chpidmat  22741  chmaidscmat  22742  cpmidgsumm2pm  22763  cpmidpmatlem2  22765  cpmidpmatlem3  22766  cpmadugsumlemB  22768  cpmadugsumfi  22771  cpmidgsum2  22773  chcoeffeqlem  22779  tlmtgp  24090  nrginvrcnlem  24586  clmvsubval  25016  cvsmuleqdivd  25041  cphsubrglem  25084  deg1pwle  26032  deg1pw  26033  ply1nz  26034  mon1pid  26066  ply1remlem  26077  dchrmulcl  27167  dchrinv  27179  dchrhash  27189  lgsqrlem1  27264  lgsqrlem2  27265  lgsqrlem3  27266  lgsqrlem4  27267  elrgspnlem2  33201  fracerl  33263  fracfld  33265  primefldgen1  33278  orng0le1  33297  ofldchr  33299  suborng  33300  isarchiofld  33302  imaslmod  33331  dvdsruasso  33363  rhmquskerlem  33403  elrspunidl  33406  elrspunsn  33407  drngidl  33411  drngidlhash  33412  rhmpreimaprmidl  33429  qsnzr  33433  ssdifidlprm  33436  mxidlprm  33448  mxidlirredi  33449  drnglidl1ne0  33453  drng0mxidl  33454  qsdrngilem  33472  qsdrnglem2  33474  rsprprmprmidl  33500  rprmasso2  33504  rprmirredlem  33508  rprmdvdsprod  33512  1arithufdlem4  33525  ressasclcl  33547  coe1mon  33561  deg1vr  33565  rlmdim  33612  rgmoddimOLD  33613  drngdimgt0  33621  extdg1id  33668  ply1annnr  33700  rtelextdg2lem  33723  submatminr1  33807  madjusmdetlem1  33824  zarcmplem  33878  zrhnm  33964  zrhchr  33971  zrhcntr  33976  qqh1  33982  qqhucn  33989  lflsub  39067  eqlkr  39099  eqlkr3  39101  lduallmodlem  39152  ldualvsubcl  39156  ldualvsubval  39157  dochfl1  41477  lcfrlem2  41544  lcdvsubval  41619  mapdpglem30  41703  hgmapval1  41894  hdmapglem5  41923  rhmzrhval  41966  aks6d1c1p6  42109  deg1gprod  42135  deg1pow  42136  aks5lem2  42182  unitscyglem5  42194  rnasclg  42494  ricdrng1  42523  fidomncyc  42530  rhmpsr  42547  evlsbagval  42561  evlsmaprhm  42565  0prjspnrel  42622  mendlmod  43185  idomodle  43187  mon1psubm  43195  deg1mhm  43196  lidldomn1  48223  mgpsumn  48355  ply1sclrmsm  48376  coe1id  48377  evl1at1  48385  linc0scn0  48416  linc1  48418  islindeps2  48476  lmod1lem5  48484  asclelbasALT  48999