Theorem ringidcl 20085

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ‘cfv 6543  Basecbs 17146  Mndcmnd 18627  mulGrpcmgp 19989  1_rcur 20006  Ringcrg 20058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  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 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-plusg 17212  df-0g 17389  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-mgp 19990  df-ur 20007  df-ring 20060

This theorem is referenced by:  ringid  20093  ringo2times  20094  ringadd2  20095  ringcomlem  20098  ringnegl  20118  ringnegr  20119  ringmneg1  20120  ringmneg2  20121  pwspjmhmmgpd  20145  imasring  20147  xpsring1d  20150  opprring  20165  dvdsrid  20185  dvdsrneg  20188  1unit  20192  ringinvdv  20232  elrhmunit  20293  isnzr2  20301  isnzr2hash  20302  0ring01eq  20308  subrgid  20325  isdrng2  20375  isdrngd  20394  isdrngdOLD  20396  abv1z  20444  abvneg  20446  srng1  20471  issrngd  20473  lmod1cl  20504  lmodvsneg  20521  lmodsubvs  20533  lmodsubdi  20534  lmodsubdir  20535  lmodprop2d  20539  rmodislmod  20545  rmodislmodOLD  20546  lssvnegcl  20572  prdslmodd  20585  lmodvsinv  20652  islmhm2  20654  lbsind2  20697  lspsneq  20741  lspexch  20748  lidl1el  20847  rsp1  20855  lpi1  20892  fidomndrnglem  20931  mulgrhm  21053  chrcl  21084  chrid  21085  chrdvds  21086  chrcong  21087  zncyg  21110  zrhpsgnelbas  21153  uvcvvcl2  21349  uvcff  21352  lindfind2  21379  sraassab  21428  asclf  21442  asclghm  21443  ascl0  21444  ascl1  21445  asclmul1  21446  asclmul2  21447  ascldimul  21448  rnascl  21451  assamulgscmlem1  21459  psrlmod  21527  psr1cl  21528  mvrf  21550  mplsubrg  21570  mplmon  21596  mplmonmul  21597  mplcoe1  21598  mplind  21637  evlslem1  21651  mhppwdeg  21699  coe1pwmul  21808  ply1scl0OLD  21820  ply1scl1OLD  21823  ply1idvr1  21824  lply1binomsc  21838  mamumat1cl  21948  mat1bas  21958  matsc  21959  mat0dimid  21977  mat1mhm  21993  dmatid  22004  scmatscmide  22016  scmatscmiddistr  22017  scmatmats  22020  scmatscm  22022  scmatid  22023  scmataddcl  22025  scmatsubcl  22026  scmatmulcl  22027  smatvscl  22033  scmatrhmcl  22037  scmatf1  22040  scmatmhm  22043  mat0scmat  22047  mat1scmat  22048  mdet0pr  22101  mdet1  22110  mdetunilem8  22128  mdetunilem9  22129  mdetuni0  22130  mdetmul  22132  m2detleiblem5  22134  m2detleiblem6  22135  maducoeval2  22149  maduf  22150  madutpos  22151  madugsum  22152  madulid  22154  minmar1marrep  22159  minmar1cl  22160  marep01ma  22169  smadiadetglem1  22180  smadiadetglem2  22181  matinv  22186  1pmatscmul  22211  1elcpmat  22224  mat2pmat1  22241  decpmatid  22279  idpm2idmp  22310  chmatcl  22337  chmatval  22338  chpmat1dlem  22344  chpmat1d  22345  chpdmatlem0  22346  chpdmatlem2  22348  chpdmatlem3  22349  chpidmat  22356  chmaidscmat  22357  cpmidgsumm2pm  22378  cpmidpmatlem2  22380  cpmidpmatlem3  22381  cpmadugsumlemB  22383  cpmadugsumfi  22386  cpmidgsum2  22388  chcoeffeqlem  22394  tlmtgp  23707  nrginvrcnlem  24215  clmvsubval  24632  cvsmuleqdivd  24657  cphsubrglem  24701  deg1pwle  25644  deg1pw  25645  ply1nz  25646  ply1remlem  25687  dchrmulcl  26759  dchrinv  26771  dchrhash  26781  lgsqrlem1  26856  lgsqrlem2  26857  lgsqrlem3  26858  lgsqrlem4  26859  dvdschrmulg  32421  frobrhm  32423  primefldgen1  32452  orng0le1  32471  ofldchr  32473  suborng  32474  isarchiofld  32476  imaslmod  32509  dvdsruasso  32535  rhmquskerlem  32588  elrspunidl  32591  elrspunsn  32592  drngidl  32596  drngidlhash  32597  rhmpreimaprmidl  32615  qsnzr  32619  mxidlprm  32631  mxidlirredi  32632  drnglidl1ne0  32636  drng0mxidl  32637  qsdrngilem  32653  qsdrnglem2  32655  asclmulg  32680  ply1chr  32706  coe1mon  32709  rlmdim  32753  rgmoddimOLD  32754  drngdimgt0  32762  extdg1id  32801  evls1maprhm  32819  ply1annnr  32824  submatminr1  32859  madjusmdetlem1  32876  zarcmplem  32930  zrhnm  33018  zrhchr  33025  qqh1  33034  qqhucn  33041  lflsub  38023  eqlkr  38055  eqlkr3  38057  lduallmodlem  38108  ldualvsubcl  38112  ldualvsubval  38113  dochfl1  40433  lcfrlem2  40500  lcdvsubval  40575  mapdpglem30  40659  hgmapval1  40850  hdmapglem5  40879  rnasclg  41159  ricdrng1  41186  rhmmpl  41207  evlsbagval  41220  evlsmaprhm  41224  0prjspnrel  41451  mendlmod  42017  idomodle  42020  isdomn3  42028  mon1pid  42029  mon1psubm  42030  deg1mhm  42031  rngisomfv1  46796  rngisom1  46797  rngisomring1  46799  rngqiprng1elbas  46850  rngqiprngghmlem1  46851  rngqiprngimf  46861  rngqiprngimf1  46864  rng2idl1cntr  46869  rngqiprngfulem1  46875  rngqiprngfulem4  46878  rngqiprngfulem5  46879  rngqiprngu  46882  lidldomn1  46902  mgpsumn  47118  ply1sclrmsm  47142  coe1id  47143  evl1at1  47151  linc0scn0  47182  linc1  47184  islindeps2  47242  lmod1lem5  47250