Theorem ringidcl 20187

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6488  Basecbs 17124  Mndcmnd 18646  mulGrpcmgp 20062  1_rcur 20103  Ringcrg 20155

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-cnex 11071  ax-resscn 11072  ax-1cn 11073  ax-icn 11074  ax-addcl 11075  ax-addrcl 11076  ax-mulcl 11077  ax-mulrcl 11078  ax-mulcom 11079  ax-addass 11080  ax-mulass 11081  ax-distr 11082  ax-i2m1 11083  ax-1ne0 11084  ax-1rid 11085  ax-rnegex 11086  ax-rrecex 11087  ax-cnre 11088  ax-pre-lttri 11089  ax-pre-lttrn 11090  ax-pre-ltadd 11091  ax-pre-mulgt0 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7311  df-ov 7357  df-oprab 7358  df-mpo 7359  df-om 7805  df-2nd 7930  df-frecs 8219  df-wrecs 8250  df-recs 8299  df-rdg 8337  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161  df-sub 11355  df-neg 11356  df-nn 12135  df-2 12197  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17125  df-plusg 17178  df-0g 17349  df-mgm 18552  df-sgrp 18631  df-mnd 18647  df-mgp 20063  df-ur 20104  df-ring 20157

This theorem is referenced by:  ringidcld  20188  ringid  20196  ringo2times  20197  ringadd2  20198  ringcomlem  20201  ringnegl  20224  ringnegr  20225  ringmneg1  20226  ringmneg2  20227  pwspjmhmmgpd  20250  imasring  20252  xpsring1d  20255  opprring  20269  dvdsrid  20289  dvdsrneg  20292  1unit  20296  ringinvdv  20336  rngisomfv1  20387  rngisom1  20388  rngisomring1  20390  elrhmunit  20429  isnzr2  20437  isnzr2hash  20438  0ring01eq  20448  subrgid  20492  rrgnz  20623  isdomn3  20634  isdrng2  20662  isdrngd  20684  isdrngdOLD  20686  fidomndrnglem  20691  abv1z  20743  abvneg  20745  srng1  20772  issrngd  20774  orng0le1  20793  suborng  20795  lmod1cl  20826  lmodvsneg  20843  lmodsubvs  20855  lmodsubdi  20856  lmodsubdir  20857  lmodprop2d  20861  rmodislmod  20867  lssvnegcl  20893  prdslmodd  20906  lmodvsinv  20974  islmhm2  20976  lbsind2  21019  lspsneq  21063  lspexch  21070  lidl1el  21167  rsp1  21178  rhmqusnsg  21226  rngqiprng1elbas  21227  rngqiprngghmlem1  21228  rngqiprngimf  21238  rngqiprngimf1  21241  rng2idl1cntr  21246  rngqiprngfulem1  21252  rngqiprngfulem4  21255  rngqiprngfulem5  21256  rngqiprngu  21259  lpi1  21268  mulgrhm  21418  chrcl  21465  chrid  21466  chrdvds  21467  chrcong  21468  dvdschrmulg  21469  zncyg  21489  frobrhm  21516  ofldchr  21517  zrhpsgnelbas  21535  uvcvvcl2  21729  uvcff  21732  lindfind2  21759  sraassab  21809  asclf  21823  asclghm  21824  ascl0  21825  ascl1  21826  asclmul1  21827  asclmul2  21828  ascldimul  21829  rnascl  21832  assamulgscmlem1  21840  asclmulg  21843  psrlmod  21900  psr1cl  21901  psrascl  21919  mvrf  21925  mplsubrg  21945  mplmon  21973  mplmonmul  21974  mplcoe1  21975  mplind  22008  evlslem1  22020  mhppwdeg  22068  psd1  22085  psdascl  22086  coe1pwmul  22196  ply1scl0OLD  22208  ply1scl1OLD  22211  ply1idvr1OLD  22213  ply1chr  22224  lply1binomsc  22229  evls1maprhm  22294  rhmmpl  22301  rhmply1vr1  22305  mamumat1cl  22357  mat1bas  22367  matsc  22368  mat0dimid  22386  mat1mhm  22402  dmatid  22413  scmatscmide  22425  scmatscmiddistr  22426  scmatmats  22429  scmatscm  22431  scmatid  22432  scmataddcl  22434  scmatsubcl  22435  scmatmulcl  22436  smatvscl  22442  scmatrhmcl  22446  scmatf1  22449  scmatmhm  22452  mat0scmat  22456  mat1scmat  22457  mdet0pr  22510  mdet1  22519  mdetunilem8  22537  mdetunilem9  22538  mdetuni0  22539  mdetmul  22541  m2detleiblem5  22543  m2detleiblem6  22544  maducoeval2  22558  maduf  22559  madutpos  22560  madugsum  22561  madulid  22563  minmar1marrep  22568  minmar1cl  22569  marep01ma  22578  smadiadetglem1  22589  smadiadetglem2  22590  matinv  22595  1pmatscmul  22620  1elcpmat  22633  mat2pmat1  22650  decpmatid  22688  idpm2idmp  22719  chmatcl  22746  chmatval  22747  chpmat1dlem  22753  chpmat1d  22754  chpdmatlem0  22755  chpdmatlem2  22757  chpdmatlem3  22758  chpidmat  22765  chmaidscmat  22766  cpmidgsumm2pm  22787  cpmidpmatlem2  22789  cpmidpmatlem3  22790  cpmadugsumlemB  22792  cpmadugsumfi  22795  cpmidgsum2  22797  chcoeffeqlem  22803  tlmtgp  24114  nrginvrcnlem  24609  clmvsubval  25039  cvsmuleqdivd  25064  cphsubrglem  25107  deg1pwle  26055  deg1pw  26056  ply1nz  26057  mon1pid  26089  ply1remlem  26100  dchrmulcl  27190  dchrinv  27202  dchrhash  27212  lgsqrlem1  27287  lgsqrlem2  27288  lgsqrlem3  27289  lgsqrlem4  27290  isarchiofld  33177  elrgspnlem2  33219  fracerl  33281  fracfld  33283  primefldgen1  33296  imaslmod  33327  dvdsruasso  33359  rhmquskerlem  33399  elrspunidl  33402  elrspunsn  33403  drngidl  33407  drngidlhash  33408  rhmpreimaprmidl  33425  qsnzr  33429  ssdifidlprm  33432  mxidlprm  33444  mxidlirredi  33445  drnglidl1ne0  33449  drng0mxidl  33450  qsdrngilem  33468  qsdrnglem2  33470  rsprprmprmidl  33496  rprmasso2  33500  rprmirredlem  33504  rprmdvdsprod  33508  1arithufdlem4  33521  ressasclcl  33543  coe1mon  33558  deg1vr  33562  rlmdim  33645  rgmoddimOLD  33646  drngdimgt0  33654  extdg1id  33702  ply1annnr  33739  rtelextdg2lem  33762  submatminr1  33846  madjusmdetlem1  33863  zarcmplem  33917  zrhnm  34003  zrhchr  34010  zrhcntr  34015  qqh1  34021  qqhucn  34028  lflsub  39189  eqlkr  39221  eqlkr3  39223  lduallmodlem  39274  ldualvsubcl  39278  ldualvsubval  39279  dochfl1  41598  lcfrlem2  41665  lcdvsubval  41740  mapdpglem30  41824  hgmapval1  42015  hdmapglem5  42044  rhmzrhval  42087  aks6d1c1p6  42230  deg1gprod  42256  deg1pow  42257  aks5lem2  42303  unitscyglem5  42315  rnasclg  42620  ricdrng1  42649  fidomncyc  42656  rhmpsr  42673  evlsbagval  42687  evlsmaprhm  42691  0prjspnrel  42748  mendlmod  43309  idomodle  43311  mon1psubm  43319  deg1mhm  43320  lidldomn1  48358  mgpsumn  48490  ply1sclrmsm  48511  coe1id  48512  evl1at1  48520  linc0scn0  48551  linc1  48553  islindeps2  48611  lmod1lem5  48619  asclelbasALT  49134