Theorem ringidcl 20344

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 2763	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20316	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringidcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20216	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringidcl.u	. . . 4 ⊢ 1 = (1r‘𝑅)
6	1, 5	ringidval 20260	. . 3 ⊢ 1 = (0g‘(mulGrp‘𝑅))
7	4, 6	mndidcl 18802	. 2 ⊢ ((mulGrp‘𝑅) ∈ Mnd → 1 ∈ 𝐵)
8	2, 7	syl 18	1 ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  Basecbs 17264  Mndcmnd 18787  mulGrpcmgp 20211  1_rcur 20258  Ringcrg 20310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-2 12298  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-plusg 17318  df-0g 17489  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-mgp 20212  df-ur 20259  df-ring 20312

This theorem is referenced by:  ringidcld  20345  ringid  20353  ringo2times  20354  ringadd2  20355  ringcomlem  20358  ringnegl  20381  ringnegr  20382  ringmneg1  20383  ringmneg2  20384  pwspjmhmmgpd  20405  imasring  20408  xpsring1d  20411  opprring  20425  dvdsrid  20445  dvdsrneg  20448  1unit  20452  ringinvdv  20492  rngisomfv1  20543  rngisom1  20544  rngisomring1  20546  elrhmunit  20607  isnzr2  20615  drnglidl1ne0  20616  isnzr2hash  20617  0ring01eq  20627  subrgid  20672  rrgnz  20803  isdomn3  20813  isdrng2  20843  isdrng3lem1  20851  isdrng3lem2  20852  isdrngd  20868  isdrngdOLD  20870  fidomndrnglem  20876  abv1z  20927  abvneg  20929  srng1  20956  issrngd  20958  orng0le1  20977  suborng  20979  lmod1cl  21010  lmodvsneg  21027  lmodsubvs  21039  lmodsubdi  21040  lmodsubdir  21041  lmodprop2d  21045  rmodislmod  21051  lssvnegcl  21077  prdslmodd  21090  lmodvsinv  21157  islmhm2  21159  lbsind2  21202  lspsneq  21246  lspexch  21253  lidl1el  21351  rsp1  21366  drngidl  21385  rhmqusnsg  21425  rngqiprng1elbas  21426  rngqiprngghmlem1  21427  rngqiprngimf  21437  rngqiprngimf1  21440  rng2idl1cntr  21445  rngqiprngfulem1  21451  rngqiprngfulem4  21454  rngqiprngfulem5  21455  rngqiprngu  21458  rhmpreimaprmidl  21479  qsnzr  21483  ssdifidlprm  21486  prmidlsubm  21487  lpi1  21495  mulgrhm  21627  chrcl  21674  chrid  21675  chrdvds  21676  chrcong  21677  dvdschrmulg  21678  zncyg  21698  frobrhm  21725  ofldchr  21726  zrhpsgnelbas  21744  uvcvvcl2  21938  uvcff  21941  lindfind2  21968  sraassab  22018  asclf  22031  asclghm  22032  ascl0  22034  ascl1  22035  asclmul1  22036  asclmul2  22037  rnascl  22041  assamulgscmlem1  22049  asclmulg  22052  psrlmod  22109  psr1cl  22110  psrascl  22128  mvrf  22134  mplsubrg  22154  mplmon  22186  mplmonmul  22187  mplcoe1  22188  mplind  22221  evlslem1  22233  evlsmaprhm  22282  mhppwdeg  22313  psd1  22330  psdascl  22331  coe1pwmul  22440  coe1id  22454  ply1chr  22466  lply1binomsc  22471  evls1maprhm  22536  rhmmpl  22540  rhmply1vr1  22544  mamumat1cl  22596  mat1bas  22606  matsc  22607  mat0dimid  22625  mat1mhm  22641  dmatid  22652  scmatscmide  22664  scmatscmiddistr  22665  scmatmats  22668  scmatscm  22670  scmatid  22671  scmataddcl  22673  scmatsubcl  22674  scmatmulcl  22675  smatvscl  22681  scmatrhmcl  22685  scmatf1  22688  scmatmhm  22691  mat0scmat  22695  mat1scmat  22696  mdet0pr  22749  mdet1  22758  mdetunilem8  22776  mdetunilem9  22777  mdetuni0  22778  mdetmul  22780  m2detleiblem5  22782  m2detleiblem6  22783  maducoeval2  22797  maduf  22798  madutpos  22799  madugsum  22800  madulid  22802  minmar1marrep  22807  minmar1cl  22808  marep01ma  22817  smadiadetglem1  22828  smadiadetglem2  22829  matinv  22834  1pmatscmul  22859  1elcpmat  22872  mat2pmat1  22889  decpmatid  22927  idpm2idmp  22958  chmatcl  22985  chmatval  22986  chpmat1dlem  22992  chpmat1d  22993  chpdmatlem0  22994  chpdmatlem2  22996  chpdmatlem3  22997  chpidmat  23004  chmaidscmat  23005  cpmidgsumm2pm  23026  cpmidpmatlem2  23028  cpmidpmatlem3  23029  cpmadugsumlemB  23031  cpmadugsumfi  23034  cpmidgsum2  23036  chcoeffeqlem  23042  tlmtgp  24353  nrginvrcnlem  24848  clmvsubval  25268  cvsmuleqdivd  25293  cphsubrglem  25336  deg1pwle  26277  deg1pw  26278  ply1nz  26279  mon1pid  26311  ply1remlem  26322  dchrmulcl  27413  dchrinv  27425  dchrhash  27435  lgsqrlem1  27510  lgsqrlem2  27511  lgsqrlem3  27512  lgsqrlem4  27513  isarchiofld  33519  elrgspnlem2  33563  fracerl  33627  fracfld  33629  primefldgen1  33642  imaslmod  33673  dvdsruasso  33698  rhmquskerlem  33733  elrspunidl  33736  elrspunsn  33737  drngidlhash  33741  mxidlprm  33753  drng0mxidl  33758  qsdrngilem  33776  qsdrnglem2  33778  rsprprmprmidl  33812  rprmasso2  33816  rprmirredlem  33820  rprmdvdsprod  33824  1arithufdlem4  33837  ressasclcl  33861  coe1mon  33877  deg1vr  33882  psrmon  33939  psrmonmul  33940  rlmdim  34000  drngdimgt0  34008  extdg1id  34056  ply1annnr  34093  rtelextdg2lem  34116  submatminr1  34200  madjusmdetlem1  34217  zarcmplem  34271  zrhnm  34357  zrhchr  34364  zrhcntr  34369  qqh1  34375  qqhucn  34382  lflsub  39841  eqlkr  39873  eqlkr3  39875  lduallmodlem  39926  ldualvsubcl  39930  ldualvsubval  39931  dochfl1  42250  lcfrlem2  42317  lcdvsubval  42392  mapdpglem30  42476  hgmapval1  42667  hdmapglem5  42696  rhmzrhval  42739  aks6d1c1p6  42881  deg1gprod  42907  deg1pow  42908  aks5lem2  42954  unitscyglem5  42966  rnasclg  43273  ricdrng1  43296  fidomncyc  43303  rhmpsr  43315  evlsbagval  43318  0prjspnrel  43359  mendlmod  43916  idomodle  43918  mon1psubm  43926  deg1mhm  43927  lidldomn1  48996  smprngprmrng  49104  isidom3  49110  mgpsumn  49143  ply1sclrmsm  49164  evl1at1  49172  linc0scn0  49203  linc1  49205  islindeps2  49263  lmod1lem5  49271  asclelbasALT  49784