Theorem ringidcl 20040

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ‘cfv 6532  Basecbs 17126  Mndcmnd 18602  mulGrpcmgp 19946  1_rcur 19963  Ringcrg 20014

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 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169

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 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 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-er 8686  df-en 8923  df-dom 8924  df-sdom 8925  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-nn 12195  df-2 12257  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17127  df-plusg 17192  df-0g 17369  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-mgp 19947  df-ur 19964  df-ring 20016

This theorem is referenced by:  ringid  20048  ringo2times  20049  ringadd2  20050  ringcomlem  20053  ringnegl  20071  ringnegr  20072  ringmneg1  20073  ringmneg2  20074  pwspjmhmmgpd  20096  imasring  20098  opprring  20113  dvdsrid  20133  dvdsrneg  20136  1unit  20140  ringinvdv  20178  elrhmunit  20239  isnzr2  20247  isnzr2hash  20248  0ring01eq  20254  isdrng2  20278  isdrngd  20297  isdrngdOLD  20299  subrgid  20314  abv1z  20389  abvneg  20391  srng1  20416  issrngd  20418  lmod1cl  20448  lmodvsneg  20465  lmodsubvs  20477  lmodsubdi  20478  lmodsubdir  20479  lmodprop2d  20483  rmodislmod  20489  rmodislmodOLD  20490  lssvnegcl  20516  prdslmodd  20529  lmodvsinv  20596  islmhm2  20598  lbsind2  20641  lspsneq  20684  lspexch  20691  lidl1el  20789  rsp1  20795  lpi1  20822  fidomndrnglem  20859  mulgrhm  20980  chrcl  21011  chrid  21012  chrdvds  21013  chrcong  21014  zncyg  21037  zrhpsgnelbas  21080  uvcvvcl2  21276  uvcff  21279  lindfind2  21306  asclf  21367  asclghm  21368  ascl0  21369  ascl1  21370  asclmul1  21371  asclmul2  21372  ascldimul  21373  rnascl  21376  assamulgscmlem1  21384  psrlmod  21452  psr1cl  21453  mvrf  21475  mplsubrg  21493  mplmon  21518  mplmonmul  21519  mplcoe1  21520  mplind  21560  evlslem1  21574  mhppwdeg  21622  coe1pwmul  21732  ply1scl0  21743  ply1scl1  21745  ply1idvr1  21746  lply1binomsc  21760  mamumat1cl  21870  mat1bas  21880  matsc  21881  mat0dimid  21899  mat1mhm  21915  dmatid  21926  scmatscmide  21938  scmatscmiddistr  21939  scmatmats  21942  scmatscm  21944  scmatid  21945  scmataddcl  21947  scmatsubcl  21948  scmatmulcl  21949  smatvscl  21955  scmatrhmcl  21959  scmatf1  21962  scmatmhm  21965  mat0scmat  21969  mat1scmat  21970  mdet0pr  22023  mdet1  22032  mdetunilem8  22050  mdetunilem9  22051  mdetuni0  22052  mdetmul  22054  m2detleiblem5  22056  m2detleiblem6  22057  maducoeval2  22071  maduf  22072  madutpos  22073  madugsum  22074  madulid  22076  minmar1marrep  22081  minmar1cl  22082  marep01ma  22091  smadiadetglem1  22102  smadiadetglem2  22103  matinv  22108  1pmatscmul  22133  1elcpmat  22146  mat2pmat1  22163  decpmatid  22201  idpm2idmp  22232  chmatcl  22259  chmatval  22260  chpmat1dlem  22266  chpmat1d  22267  chpdmatlem0  22268  chpdmatlem2  22270  chpdmatlem3  22271  chpidmat  22278  chmaidscmat  22279  cpmidgsumm2pm  22300  cpmidpmatlem2  22302  cpmidpmatlem3  22303  cpmadugsumlemB  22305  cpmadugsumfi  22308  cpmidgsum2  22310  chcoeffeqlem  22316  tlmtgp  23629  nrginvrcnlem  24137  clmvsubval  24554  cvsmuleqdivd  24579  cphsubrglem  24623  deg1pwle  25566  deg1pw  25567  ply1nz  25568  ply1remlem  25609  dchrmulcl  26679  dchrinv  26691  dchrhash  26701  lgsqrlem1  26776  lgsqrlem2  26777  lgsqrlem3  26778  lgsqrlem4  26779  dvdschrmulg  32248  frobrhm  32250  primefldgen1  32273  orng0le1  32292  ofldchr  32294  suborng  32295  isarchiofld  32297  imaslmod  32330  rhmqusker  32395  elrspunidl  32397  elrspunsn  32398  drngidl  32402  drngidlhash  32403  rhmpreimaprmidl  32421  qsnzr  32425  mxidlprm  32437  qsdrngilem  32454  qsdrnglem2  32456  asclmulg  32480  ply1chr  32501  coe1mon  32504  rgmoddim  32533  drngdimgt0  32541  extdg1id  32580  evls1maprhm  32596  submatminr1  32621  madjusmdetlem1  32638  zarcmplem  32692  zrhnm  32780  zrhchr  32787  qqh1  32796  qqhucn  32803  lflsub  37742  eqlkr  37774  eqlkr3  37776  lduallmodlem  37827  ldualvsubcl  37831  ldualvsubval  37832  dochfl1  40152  lcfrlem2  40219  lcdvsubval  40294  mapdpglem30  40378  hgmapval1  40569  hdmapglem5  40598  rnasclg  40880  ricdrng1  40906  rhmmpl  40927  evlsbagval  40934  mhphf  40957  0prjspnrel  41151  mendlmod  41706  idomodle  41709  isdomn3  41717  mon1pid  41718  mon1psubm  41719  deg1mhm  41720  lidldomn1  46467  mgpsumn  46687  ply1sclrmsm  46712  coe1id  46713  evl1at1  46721  linc0scn0  46752  linc1  46754  islindeps2  46812  lmod1lem5  46820