Theorem ringidcl 20487

Description: The unity element of a ring belongs to the base set of the ring. (Contributed by FL, 12-Feb-2010.) (Revised 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 2761	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20458	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringidcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20358	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringidcl.u	. . . 4 ⊢ 1 = (1r‘𝑅)
6	1, 5	ringidval 20402	. . 3 ⊢ 1 = (0g‘(mulGrp‘𝑅))
7	4, 6	mndidcl 18932	. 2 ⊢ ((mulGrp‘𝑅) ∈ Mnd → 1 ∈ 𝐵)
8	2, 7	syl 18	1 ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  Basecbs 17380  Mndcmnd 18916  mulGrpcmgp 20353  1_rcur 20400  Ringcrg 20452

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-2 12398  df-sets 17335  df-slot 17353  df-ndx 17365  df-base 17381  df-plusg 17434  df-0g 17605  df-mgm 18809  df-sgrp 18901  df-mnd 18917  df-mgp 20354  df-ur 20401  df-ring 20454

This theorem is used by:  ringidcld  20488  ringid  20496  ringo2times  20497  ringadd2  20498  ringcomlem  20501  ringnegl  20526  ringnegr  20527  ringmneg1  20528  ringmneg2  20529  pwspjmhmmgpd  20550  imasring  20553  xpsring1d  20556  opprring  20570  dvdsrid  20590  dvdsrneg  20593  1unit  20597  ringinvdv  20637  rngisomfv1  20688  rngisom1  20689  rngisomring1  20691  elrhmunit  20753  isnzr2  20761  drnglidl1ne0  20762  isnzr2hash  20763  0ring01eq  20773  subrgid  20818  rrgnz  20949  isdomn3  20959  isdrng2  20990  isdrng3lem1  20998  isdrng3lem2  20999  isdrngd  21015  isdrngdOLD  21017  fidomndrnglem  21023  abv1z  21074  abvneg  21076  srng1  21103  issrngd  21105  orng0le1  21124  suborng  21126  lmod1cl  21157  lmodvsneg  21174  lmodsubvs  21186  lmodsubdi  21187  lmodsubdir  21188  lmodprop2d  21192  rmodislmod  21198  lssvnegcl  21224  prdslmodd  21237  lmodvsinv  21304  islmhm2  21306  lbsind2  21349  lspsneq  21393  lspexch  21400  lidl1el  21498  rsp1  21513  drngidl  21532  rhmqusnsg  21574  rngqiprng1elbas  21575  rngqiprngghmlem1  21576  rngqiprngimf  21586  rngqiprngimf1  21589  rng2idl1cntr  21594  rngqiprngfulem1  21600  rngqiprngfulem4  21603  rngqiprngfulem5  21604  rngqiprngu  21607  rhmpreimaprmidl  21628  qsnzr  21632  ssdifidlprm  21635  prmidlsubm  21636  lpi1  21644  mulgrhm  21776  chrcl  21823  chrid  21824  chrdvds  21825  chrcong  21826  dvdschrmulg  21827  zncyg  21847  frobrhm  21874  ofldchr  21875  zrhpsgnelbas  21893  uvcvvcl2  22087  uvcff  22090  lindfind2  22117  sraassab  22169  asclf  22182  asclghm  22183  ascl0  22185  ascl1  22186  asclmul1  22187  asclmul2  22188  rnascl  22192  assamulgscmlem1  22200  asclmulg  22203  psrlmod  22260  psr1cl  22261  psrascl  22279  mvrf  22285  mplsubrg  22305  mplmon  22337  mplmonmul  22338  mplcoe1  22339  mplind  22372  evlslem1  22384  evlsmaprhm  22433  mhppwdeg  22464  psd1  22481  psdascl  22482  coe1pwmul  22591  coe1id  22605  ply1chr  22617  lply1binomsc  22622  evls1maprhm  22687  rhmmpl  22691  rhmply1vr1  22695  mamumat1cl  22747  mat1bas  22757  matsc  22758  mat0dimid  22776  mat1mhm  22792  dmatid  22803  scmatscmide  22815  scmatscmiddistr  22816  scmatmats  22819  scmatscm  22821  scmatid  22822  scmataddcl  22824  scmatsubcl  22825  scmatmulcl  22826  smatvscl  22832  scmatrhmcl  22836  scmatf1  22839  scmatmhm  22842  mat0scmat  22846  mat1scmat  22847  mdet0pr  22900  mdet1  22909  mdetunilem8  22927  mdetunilem9  22928  mdetuni0  22929  mdetmul  22931  m2detleiblem5  22933  m2detleiblem6  22934  maducoeval2  22948  maduf  22949  madutpos  22950  madugsum  22951  madulid  22953  minmar1marrep  22958  minmar1cl  22959  marep01ma  22968  smadiadetglem1  22979  smadiadetglem2  22980  matinv  22985  1pmatscmul  23013  1elcpmat  23026  mat2pmat1  23043  decpmatid  23081  idpm2idmp  23112  chmatcl  23139  chmatval  23140  chpmat1dlem  23146  chpmat1d  23147  chpdmatlem0  23148  chpdmatlem2  23150  chpdmatlem3  23151  chpidmat  23158  chmaidscmat  23159  cpmidgsumm2pm  23180  cpmidpmatlem2  23182  cpmidpmatlem3  23183  cpmadugsumlemB  23185  cpmadugsumfi  23188  cpmidgsum2  23190  chcoeffeqlem  23196  tlmtgp  24508  nrginvrcnlem  25003  clmvsubval  25423  cvsmuleqdivd  25448  cphsubrglem  25491  deg1pwle  26431  deg1pw  26432  ply1nz  26433  mon1pid  26465  ply1remlem  26476  dchrmulcl  27569  dchrinv  27581  dchrhash  27591  lgsqrlem1  27666  lgsqrlem2  27667  lgsqrlem3  27668  lgsqrlem4  27669  isarchiofld  33753  elrgspnlem2  33797  fracerl  33861  fracfld  33863  primefldgen1  33876  imaslmod  33907  dvdsruasso  33933  rhmquskerlem  33968  elrspunidl  33971  elrspunsn  33972  drngidlhash  33976  mxidlprm  33988  drng0mxidl  33993  qsdrngilem  34011  qsdrnglem2  34013  rsprprmprmidl  34047  rprmasso2  34051  rprmirredlem  34055  rprmdvdsprod  34059  1arithufdlem4  34072  ressasclcl  34096  coe1mon  34112  deg1vr  34117  psrmon  34174  psrmonmul  34175  rlmdim  34235  drngdimgt0  34243  extdg1id  34291  ply1annnr  34328  rtelextdg2lem  34351  submatminr1  34435  madjusmdetlem1  34452  zarcmplem  34506  zrhnm  34592  zrhchr  34599  zrhcntr  34604  qqh1  34610  qqhucn  34617  lflsub  40104  eqlkr  40136  eqlkr3  40138  lduallmodlem  40189  ldualvsubcl  40193  ldualvsubval  40194  dochfl1  42513  lcfrlem2  42580  lcdvsubval  42655  mapdpglem30  42739  hgmapval1  42930  hdmapglem5  42959  rhmzrhval  43002  aks6d1c1p6  43144  deg1gprod  43170  deg1pow  43171  aks5lem2  43217  unitscyglem5  43229  rnasclg  43543  ricdrng1  43572  fidomncyc  43579  rhmpsr  43591  evlsbagval  43594  0prjspnrel  43643  mendlmod  44175  idomodle  44177  mon1psubm  44185  deg1mhm  44186  lidldomn1  49297  smprngprmrng  49405  isidom3  49411  mgpsumn  49444  ply1sclrmsm  49465  evl1at1  49473  linc0scn0  49504  linc1  49506  islindeps2  49564  lmod1lem5  49572  asclelbasALT  50083