Theorem ringidcl 20155

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  ‘cfv 6543  Basecbs 17149  Mndcmnd 18660  mulGrpcmgp 20029  1_rcur 20076  Ringcrg 20128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-2 12280  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-plusg 17215  df-0g 17392  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-mgp 20030  df-ur 20077  df-ring 20130

This theorem is referenced by:  ringid  20163  ringo2times  20164  ringadd2  20165  ringcomlem  20168  ringnegl  20191  ringnegr  20192  ringmneg1  20193  ringmneg2  20194  pwspjmhmmgpd  20217  imasring  20219  xpsring1d  20222  opprring  20239  dvdsrid  20259  dvdsrneg  20262  1unit  20266  ringinvdv  20306  rngisomfv1  20357  rngisom1  20358  rngisomring1  20360  elrhmunit  20402  isnzr2  20410  isnzr2hash  20411  0ring01eq  20419  subrgid  20464  isdrng2  20515  isdrngd  20534  isdrngdOLD  20536  abv1z  20584  abvneg  20586  srng1  20611  issrngd  20613  lmod1cl  20644  lmodvsneg  20661  lmodsubvs  20673  lmodsubdi  20674  lmodsubdir  20675  lmodprop2d  20679  rmodislmod  20685  rmodislmodOLD  20686  lssvnegcl  20712  prdslmodd  20725  lmodvsinv  20792  islmhm2  20794  lbsind2  20837  lspsneq  20881  lspexch  20888  lidl1el  20991  rsp1  20999  rngqiprng1elbas  21046  rngqiprngghmlem1  21047  rngqiprngimf  21057  rngqiprngimf1  21060  rng2idl1cntr  21065  rngqiprngfulem1  21071  rngqiprngfulem4  21074  rngqiprngfulem5  21075  rngqiprngu  21078  lpi1  21087  fidomndrnglem  21126  mulgrhm  21249  chrcl  21298  chrid  21299  chrdvds  21300  chrcong  21301  zncyg  21324  zrhpsgnelbas  21367  uvcvvcl2  21563  uvcff  21566  lindfind2  21593  sraassab  21642  asclf  21656  asclghm  21657  ascl0  21658  ascl1  21659  asclmul1  21660  asclmul2  21661  ascldimul  21662  rnascl  21665  assamulgscmlem1  21673  psrlmod  21741  psr1cl  21742  mvrf  21764  mplsubrg  21784  mplmon  21810  mplmonmul  21811  mplcoe1  21812  mplind  21851  evlslem1  21865  mhppwdeg  21913  coe1pwmul  22022  ply1scl0OLD  22034  ply1scl1OLD  22037  ply1idvr1  22038  lply1binomsc  22052  mamumat1cl  22162  mat1bas  22172  matsc  22173  mat0dimid  22191  mat1mhm  22207  dmatid  22218  scmatscmide  22230  scmatscmiddistr  22231  scmatmats  22234  scmatscm  22236  scmatid  22237  scmataddcl  22239  scmatsubcl  22240  scmatmulcl  22241  smatvscl  22247  scmatrhmcl  22251  scmatf1  22254  scmatmhm  22257  mat0scmat  22261  mat1scmat  22262  mdet0pr  22315  mdet1  22324  mdetunilem8  22342  mdetunilem9  22343  mdetuni0  22344  mdetmul  22346  m2detleiblem5  22348  m2detleiblem6  22349  maducoeval2  22363  maduf  22364  madutpos  22365  madugsum  22366  madulid  22368  minmar1marrep  22373  minmar1cl  22374  marep01ma  22383  smadiadetglem1  22394  smadiadetglem2  22395  matinv  22400  1pmatscmul  22425  1elcpmat  22438  mat2pmat1  22455  decpmatid  22493  idpm2idmp  22524  chmatcl  22551  chmatval  22552  chpmat1dlem  22558  chpmat1d  22559  chpdmatlem0  22560  chpdmatlem2  22562  chpdmatlem3  22563  chpidmat  22570  chmaidscmat  22571  cpmidgsumm2pm  22592  cpmidpmatlem2  22594  cpmidpmatlem3  22595  cpmadugsumlemB  22597  cpmadugsumfi  22600  cpmidgsum2  22602  chcoeffeqlem  22608  tlmtgp  23921  nrginvrcnlem  24429  clmvsubval  24857  cvsmuleqdivd  24882  cphsubrglem  24926  deg1pwle  25873  deg1pw  25874  ply1nz  25875  ply1remlem  25916  dchrmulcl  26989  dchrinv  27001  dchrhash  27011  lgsqrlem1  27086  lgsqrlem2  27087  lgsqrlem3  27088  lgsqrlem4  27089  dvdschrmulg  32651  frobrhm  32653  primefldgen1  32682  orng0le1  32701  ofldchr  32703  suborng  32704  isarchiofld  32706  imaslmod  32739  dvdsruasso  32765  rhmquskerlem  32818  elrspunidl  32821  elrspunsn  32822  drngidl  32826  drngidlhash  32827  rhmpreimaprmidl  32845  qsnzr  32849  mxidlprm  32861  mxidlirredi  32862  drnglidl1ne0  32866  drng0mxidl  32867  qsdrngilem  32883  qsdrnglem2  32885  asclmulg  32910  ply1chr  32936  coe1mon  32939  rlmdim  32983  rgmoddimOLD  32984  drngdimgt0  32992  extdg1id  33031  evls1maprhm  33049  ply1annnr  33054  submatminr1  33089  madjusmdetlem1  33106  zarcmplem  33160  zrhnm  33248  zrhchr  33255  qqh1  33264  qqhucn  33271  lflsub  38241  eqlkr  38273  eqlkr3  38275  lduallmodlem  38326  ldualvsubcl  38330  ldualvsubval  38331  dochfl1  40651  lcfrlem2  40718  lcdvsubval  40793  mapdpglem30  40877  hgmapval1  41068  hdmapglem5  41097  rnasclg  41380  ricdrng1  41407  rhmmpl  41428  evlsbagval  41441  evlsmaprhm  41445  0prjspnrel  41672  mendlmod  42238  idomodle  42241  isdomn3  42249  mon1pid  42250  mon1psubm  42251  deg1mhm  42252  lidldomn1  46912  mgpsumn  47128  ply1sclrmsm  47152  coe1id  47153  evl1at1  47161  linc0scn0  47192  linc1  47194  islindeps2  47252  lmod1lem5  47260