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 2737	. . 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 1542   ∈ wcel 2114  ‘cfv 6492  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  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 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  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  20478  isnzr2  20486  isnzr2hash  20487  0ring01eq  20497  subrgid  20541  rrgnz  20672  isdomn3  20683  isdrng2  20711  isdrngd  20733  isdrngdOLD  20735  fidomndrnglem  20740  abv1z  20792  abvneg  20794  srng1  20821  issrngd  20823  orng0le1  20842  suborng  20844  lmod1cl  20875  lmodvsneg  20892  lmodsubvs  20904  lmodsubdi  20905  lmodsubdir  20906  lmodprop2d  20910  rmodislmod  20916  lssvnegcl  20942  prdslmodd  20955  lmodvsinv  21023  islmhm2  21025  lbsind2  21068  lspsneq  21112  lspexch  21119  lidl1el  21216  rsp1  21227  rhmqusnsg  21275  rngqiprng1elbas  21276  rngqiprngghmlem1  21277  rngqiprngimf  21287  rngqiprngimf1  21290  rng2idl1cntr  21295  rngqiprngfulem1  21301  rngqiprngfulem4  21304  rngqiprngfulem5  21305  rngqiprngu  21308  lpi1  21317  mulgrhm  21467  chrcl  21514  chrid  21515  chrdvds  21516  chrcong  21517  dvdschrmulg  21518  zncyg  21538  frobrhm  21565  ofldchr  21566  zrhpsgnelbas  21584  uvcvvcl2  21778  uvcff  21781  lindfind2  21808  sraassab  21858  asclf  21871  asclghm  21872  ascl0  21874  ascl1  21875  asclmul1  21876  asclmul2  21877  ascldimul  21878  rnascl  21881  assamulgscmlem1  21889  asclmulg  21892  psrlmod  21948  psr1cl  21949  psrascl  21967  mvrf  21973  mplsubrg  21993  mplmon  22023  mplmonmul  22024  mplcoe1  22025  mplind  22058  evlslem1  22070  mhppwdeg  22126  psd1  22143  psdascl  22144  coe1pwmul  22254  coe1id  22268  ply1idvr1OLD  22270  ply1chr  22281  lply1binomsc  22286  evls1maprhm  22351  rhmmpl  22358  rhmply1vr1  22362  mamumat1cl  22414  mat1bas  22424  matsc  22425  mat0dimid  22443  mat1mhm  22459  dmatid  22470  scmatscmide  22482  scmatscmiddistr  22483  scmatmats  22486  scmatscm  22488  scmatid  22489  scmataddcl  22491  scmatsubcl  22492  scmatmulcl  22493  smatvscl  22499  scmatrhmcl  22503  scmatf1  22506  scmatmhm  22509  mat0scmat  22513  mat1scmat  22514  mdet0pr  22567  mdet1  22576  mdetunilem8  22594  mdetunilem9  22595  mdetuni0  22596  mdetmul  22598  m2detleiblem5  22600  m2detleiblem6  22601  maducoeval2  22615  maduf  22616  madutpos  22617  madugsum  22618  madulid  22620  minmar1marrep  22625  minmar1cl  22626  marep01ma  22635  smadiadetglem1  22646  smadiadetglem2  22647  matinv  22652  1pmatscmul  22677  1elcpmat  22690  mat2pmat1  22707  decpmatid  22745  idpm2idmp  22776  chmatcl  22803  chmatval  22804  chpmat1dlem  22810  chpmat1d  22811  chpdmatlem0  22812  chpdmatlem2  22814  chpdmatlem3  22815  chpidmat  22822  chmaidscmat  22823  cpmidgsumm2pm  22844  cpmidpmatlem2  22846  cpmidpmatlem3  22847  cpmadugsumlemB  22849  cpmadugsumfi  22852  cpmidgsum2  22854  chcoeffeqlem  22860  tlmtgp  24171  nrginvrcnlem  24666  clmvsubval  25086  cvsmuleqdivd  25111  cphsubrglem  25154  deg1pwle  26095  deg1pw  26096  ply1nz  26097  mon1pid  26129  ply1remlem  26140  dchrmulcl  27226  dchrinv  27238  dchrhash  27248  lgsqrlem1  27323  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  isarchiofld  33275  elrgspnlem2  33319  fracerl  33382  fracfld  33384  primefldgen1  33397  imaslmod  33428  dvdsruasso  33460  rhmquskerlem  33500  elrspunidl  33503  elrspunsn  33504  drngidl  33508  drngidlhash  33509  rhmpreimaprmidl  33526  qsnzr  33530  ssdifidlprm  33533  mxidlprm  33545  mxidlirredi  33546  drnglidl1ne0  33550  drng0mxidl  33551  qsdrngilem  33569  qsdrnglem2  33571  rsprprmprmidl  33597  rprmasso2  33601  rprmirredlem  33605  rprmdvdsprod  33609  1arithufdlem4  33622  ressasclcl  33646  coe1mon  33662  deg1vr  33667  psrmon  33708  psrmonmul  33709  rlmdim  33769  rgmoddimOLD  33770  drngdimgt0  33778  extdg1id  33826  ply1annnr  33863  rtelextdg2lem  33886  submatminr1  33970  madjusmdetlem1  33987  zarcmplem  34041  zrhnm  34127  zrhchr  34134  zrhcntr  34139  qqh1  34145  qqhucn  34152  lflsub  39527  eqlkr  39559  eqlkr3  39561  lduallmodlem  39612  ldualvsubcl  39616  ldualvsubval  39617  dochfl1  41936  lcfrlem2  42003  lcdvsubval  42078  mapdpglem30  42162  hgmapval1  42353  hdmapglem5  42382  rhmzrhval  42425  aks6d1c1p6  42567  deg1gprod  42593  deg1pow  42594  aks5lem2  42640  unitscyglem5  42652  rnasclg  42958  ricdrng1  42987  fidomncyc  42994  rhmpsr  43009  evlsbagval  43016  evlsmaprhm  43020  0prjspnrel  43074  mendlmod  43635  idomodle  43637  mon1psubm  43645  deg1mhm  43646  lidldomn1  48719  mgpsumn  48851  ply1sclrmsm  48872  evl1at1  48880  linc0scn0  48911  linc1  48913  islindeps2  48971  lmod1lem5  48979  asclelbasALT  49493