Theorem ringidcl 20237

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  Basecbs 17170  Mndcmnd 18693  mulGrpcmgp 20112  1_rcur 20153  Ringcrg 20205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-plusg 17224  df-0g 17395  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mgp 20113  df-ur 20154  df-ring 20207

This theorem is referenced by:  ringidcld  20238  ringid  20246  ringo2times  20247  ringadd2  20248  ringcomlem  20251  ringnegl  20274  ringnegr  20275  ringmneg1  20276  ringmneg2  20277  pwspjmhmmgpd  20298  imasring  20301  xpsring1d  20304  opprring  20318  dvdsrid  20338  dvdsrneg  20341  1unit  20345  ringinvdv  20385  rngisomfv1  20436  rngisom1  20437  rngisomring1  20439  elrhmunit  20482  isnzr2  20490  isnzr2hash  20491  0ring01eq  20501  subrgid  20545  rrgnz  20676  isdomn3  20687  isdrng2  20715  isdrngd  20737  isdrngdOLD  20739  fidomndrnglem  20744  abv1z  20796  abvneg  20798  srng1  20825  issrngd  20827  orng0le1  20846  suborng  20848  lmod1cl  20879  lmodvsneg  20896  lmodsubvs  20908  lmodsubdi  20909  lmodsubdir  20910  lmodprop2d  20914  rmodislmod  20920  lssvnegcl  20946  prdslmodd  20959  lmodvsinv  21026  islmhm2  21028  lbsind2  21071  lspsneq  21115  lspexch  21122  lidl1el  21219  rsp1  21230  rhmqusnsg  21278  rngqiprng1elbas  21279  rngqiprngghmlem1  21280  rngqiprngimf  21290  rngqiprngimf1  21293  rng2idl1cntr  21298  rngqiprngfulem1  21304  rngqiprngfulem4  21307  rngqiprngfulem5  21308  rngqiprngu  21311  lpi1  21320  mulgrhm  21452  chrcl  21499  chrid  21500  chrdvds  21501  chrcong  21502  dvdschrmulg  21503  zncyg  21523  frobrhm  21550  ofldchr  21551  zrhpsgnelbas  21569  uvcvvcl2  21763  uvcff  21766  lindfind2  21793  sraassab  21843  asclf  21856  asclghm  21857  ascl0  21859  ascl1  21860  asclmul1  21861  asclmul2  21862  ascldimul  21863  rnascl  21866  assamulgscmlem1  21874  asclmulg  21877  psrlmod  21934  psr1cl  21935  psrascl  21953  mvrf  21959  mplsubrg  21979  mplmon  22011  mplmonmul  22012  mplcoe1  22013  mplind  22046  evlslem1  22058  evlsmaprhm  22107  mhppwdeg  22138  psd1  22155  psdascl  22156  coe1pwmul  22265  coe1id  22279  ply1idvr1OLD  22281  ply1chr  22292  lply1binomsc  22297  evls1maprhm  22362  rhmmpl  22366  rhmply1vr1  22370  mamumat1cl  22422  mat1bas  22432  matsc  22433  mat0dimid  22451  mat1mhm  22467  dmatid  22478  scmatscmide  22490  scmatscmiddistr  22491  scmatmats  22494  scmatscm  22496  scmatid  22497  scmataddcl  22499  scmatsubcl  22500  scmatmulcl  22501  smatvscl  22507  scmatrhmcl  22511  scmatf1  22514  scmatmhm  22517  mat0scmat  22521  mat1scmat  22522  mdet0pr  22575  mdet1  22584  mdetunilem8  22602  mdetunilem9  22603  mdetuni0  22604  mdetmul  22606  m2detleiblem5  22608  m2detleiblem6  22609  maducoeval2  22623  maduf  22624  madutpos  22625  madugsum  22626  madulid  22628  minmar1marrep  22633  minmar1cl  22634  marep01ma  22643  smadiadetglem1  22654  smadiadetglem2  22655  matinv  22660  1pmatscmul  22685  1elcpmat  22698  mat2pmat1  22715  decpmatid  22753  idpm2idmp  22784  chmatcl  22811  chmatval  22812  chpmat1dlem  22818  chpmat1d  22819  chpdmatlem0  22820  chpdmatlem2  22822  chpdmatlem3  22823  chpidmat  22830  chmaidscmat  22831  cpmidgsumm2pm  22852  cpmidpmatlem2  22854  cpmidpmatlem3  22855  cpmadugsumlemB  22857  cpmadugsumfi  22860  cpmidgsum2  22862  chcoeffeqlem  22868  tlmtgp  24179  nrginvrcnlem  24674  clmvsubval  25094  cvsmuleqdivd  25119  cphsubrglem  25162  deg1pwle  26103  deg1pw  26104  ply1nz  26105  mon1pid  26137  ply1remlem  26148  dchrmulcl  27230  dchrinv  27242  dchrhash  27252  lgsqrlem1  27327  lgsqrlem2  27328  lgsqrlem3  27329  lgsqrlem4  27330  isarchiofld  33280  elrgspnlem2  33324  fracerl  33390  fracfld  33392  primefldgen1  33405  imaslmod  33436  dvdsruasso  33468  rhmquskerlem  33508  elrspunidl  33511  elrspunsn  33512  drngidl  33516  drngidlhash  33517  rhmpreimaprmidl  33534  qsnzr  33538  ssdifidlprm  33541  mxidlprm  33553  mxidlirredi  33554  drnglidl1ne0  33558  drng0mxidl  33559  qsdrngilem  33577  qsdrnglem2  33579  rsprprmprmidl  33605  rprmasso2  33609  rprmirredlem  33613  rprmdvdsprod  33617  1arithufdlem4  33630  ressasclcl  33654  coe1mon  33670  deg1vr  33675  psrmon  33733  psrmonmul  33734  rlmdim  33794  drngdimgt0  33802  extdg1id  33850  ply1annnr  33887  rtelextdg2lem  33910  submatminr1  33994  madjusmdetlem1  34011  zarcmplem  34065  zrhnm  34151  zrhchr  34158  zrhcntr  34163  qqh1  34169  qqhucn  34176  lflsub  39559  eqlkr  39591  eqlkr3  39593  lduallmodlem  39644  ldualvsubcl  39648  ldualvsubval  39649  dochfl1  41968  lcfrlem2  42035  lcdvsubval  42110  mapdpglem30  42194  hgmapval1  42385  hdmapglem5  42414  rhmzrhval  42457  aks6d1c1p6  42599  deg1gprod  42625  deg1pow  42626  aks5lem2  42672  unitscyglem5  42684  rnasclg  42989  ricdrng1  43014  fidomncyc  43021  rhmpsr  43033  evlsbagval  43036  0prjspnrel  43077  mendlmod  43634  idomodle  43636  mon1psubm  43644  deg1mhm  43645  lidldomn1  48722  mgpsumn  48854  ply1sclrmsm  48875  evl1at1  48883  linc0scn0  48914  linc1  48916  islindeps2  48974  lmod1lem5  48982  asclelbasALT  49496