Theorem ringidcl 20279

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  Basecbs 17244  Mndcmnd 18759  mulGrpcmgp 20151  1_rcur 20198  Ringcrg 20250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-plusg 17310  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mgp 20152  df-ur 20199  df-ring 20252

This theorem is referenced by:  ringid  20287  ringo2times  20288  ringadd2  20289  ringcomlem  20292  ringnegl  20315  ringnegr  20316  ringmneg1  20317  ringmneg2  20318  pwspjmhmmgpd  20341  imasring  20343  xpsring1d  20346  opprring  20363  dvdsrid  20383  dvdsrneg  20386  1unit  20390  ringinvdv  20430  rngisomfv1  20481  rngisom1  20482  rngisomring1  20484  elrhmunit  20526  isnzr2  20534  isnzr2hash  20535  0ring01eq  20545  subrgid  20589  rrgnz  20720  isdomn3  20731  isdrng2  20759  isdrngd  20781  isdrngdOLD  20783  fidomndrnglem  20789  abv1z  20841  abvneg  20843  srng1  20870  issrngd  20872  lmod1cl  20903  lmodvsneg  20920  lmodsubvs  20932  lmodsubdi  20933  lmodsubdir  20934  lmodprop2d  20938  rmodislmod  20944  rmodislmodOLD  20945  lssvnegcl  20971  prdslmodd  20984  lmodvsinv  21052  islmhm2  21054  lbsind2  21097  lspsneq  21141  lspexch  21148  lidl1el  21253  rsp1  21264  rhmqusnsg  21312  rngqiprng1elbas  21313  rngqiprngghmlem1  21314  rngqiprngimf  21324  rngqiprngimf1  21327  rng2idl1cntr  21332  rngqiprngfulem1  21338  rngqiprngfulem4  21341  rngqiprngfulem5  21342  rngqiprngu  21345  lpi1  21354  mulgrhm  21505  chrcl  21556  chrid  21557  chrdvds  21558  chrcong  21559  dvdschrmulg  21560  zncyg  21584  frobrhm  21611  zrhpsgnelbas  21629  uvcvvcl2  21825  uvcff  21828  lindfind2  21855  sraassab  21905  asclf  21919  asclghm  21920  ascl0  21921  ascl1  21922  asclmul1  21923  asclmul2  21924  ascldimul  21925  rnascl  21928  assamulgscmlem1  21936  asclmulg  21939  psrlmod  21997  psr1cl  21998  psrascl  22016  mvrf  22022  mplsubrg  22042  mplmon  22070  mplmonmul  22071  mplcoe1  22072  mplind  22111  evlslem1  22123  mhppwdeg  22171  psd1  22188  psdascl  22189  coe1pwmul  22297  ply1scl0OLD  22309  ply1scl1OLD  22312  ply1idvr1OLD  22314  ply1chr  22325  lply1binomsc  22330  evls1maprhm  22395  rhmmpl  22402  rhmply1vr1  22406  mamumat1cl  22460  mat1bas  22470  matsc  22471  mat0dimid  22489  mat1mhm  22505  dmatid  22516  scmatscmide  22528  scmatscmiddistr  22529  scmatmats  22532  scmatscm  22534  scmatid  22535  scmataddcl  22537  scmatsubcl  22538  scmatmulcl  22539  smatvscl  22545  scmatrhmcl  22549  scmatf1  22552  scmatmhm  22555  mat0scmat  22559  mat1scmat  22560  mdet0pr  22613  mdet1  22622  mdetunilem8  22640  mdetunilem9  22641  mdetuni0  22642  mdetmul  22644  m2detleiblem5  22646  m2detleiblem6  22647  maducoeval2  22661  maduf  22662  madutpos  22663  madugsum  22664  madulid  22666  minmar1marrep  22671  minmar1cl  22672  marep01ma  22681  smadiadetglem1  22692  smadiadetglem2  22693  matinv  22698  1pmatscmul  22723  1elcpmat  22736  mat2pmat1  22753  decpmatid  22791  idpm2idmp  22822  chmatcl  22849  chmatval  22850  chpmat1dlem  22856  chpmat1d  22857  chpdmatlem0  22858  chpdmatlem2  22860  chpdmatlem3  22861  chpidmat  22868  chmaidscmat  22869  cpmidgsumm2pm  22890  cpmidpmatlem2  22892  cpmidpmatlem3  22893  cpmadugsumlemB  22895  cpmadugsumfi  22898  cpmidgsum2  22900  chcoeffeqlem  22906  tlmtgp  24219  nrginvrcnlem  24727  clmvsubval  25155  cvsmuleqdivd  25180  cphsubrglem  25224  deg1pwle  26173  deg1pw  26174  ply1nz  26175  mon1pid  26207  ply1remlem  26218  dchrmulcl  27307  dchrinv  27319  dchrhash  27329  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  elrgspnlem2  33232  fracerl  33287  fracfld  33289  primefldgen1  33302  orng0le1  33321  ofldchr  33323  suborng  33324  isarchiofld  33326  imaslmod  33360  dvdsruasso  33392  rhmquskerlem  33432  elrspunidl  33435  elrspunsn  33436  drngidl  33440  drngidlhash  33441  rhmpreimaprmidl  33458  qsnzr  33462  ssdifidlprm  33465  mxidlprm  33477  mxidlirredi  33478  drnglidl1ne0  33482  drng0mxidl  33483  qsdrngilem  33501  qsdrnglem2  33503  rsprprmprmidl  33529  rprmasso2  33533  rprmirredlem  33537  rprmdvdsprod  33541  1arithufdlem4  33554  ressasclcl  33575  coe1mon  33589  deg1vr  33593  rlmdim  33636  rgmoddimOLD  33637  drngdimgt0  33645  extdg1id  33690  ply1annnr  33710  rtelextdg2lem  33731  submatminr1  33770  madjusmdetlem1  33787  zarcmplem  33841  zrhnm  33929  zrhchr  33936  zrhcntr  33941  qqh1  33947  qqhucn  33954  lflsub  39048  eqlkr  39080  eqlkr3  39082  lduallmodlem  39133  ldualvsubcl  39137  ldualvsubval  39138  dochfl1  41458  lcfrlem2  41525  lcdvsubval  41600  mapdpglem30  41684  hgmapval1  41875  hdmapglem5  41904  rhmzrhval  41951  aks6d1c1p6  42095  deg1gprod  42121  deg1pow  42122  aks5lem2  42168  unitscyglem5  42180  rnasclg  42485  ricdrng1  42514  fidomncyc  42521  rhmpsr  42538  evlsbagval  42552  evlsmaprhm  42556  0prjspnrel  42613  mendlmod  43177  idomodle  43179  mon1psubm  43187  deg1mhm  43188  lidldomn1  48074  mgpsumn  48207  ply1sclrmsm  48228  coe1id  48229  evl1at1  48237  linc0scn0  48268  linc1  48270  islindeps2  48328  lmod1lem5  48336  asclelbasALT  48795