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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ‘cfv 6533  Basecbs 17265  Mndcmnd 18788  mulGrpcmgp 20212  1_rcur 20259  Ringcrg 20311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  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 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-nn 12230  df-2 12299  df-sets 17220  df-slot 17238  df-ndx 17250  df-base 17266  df-plusg 17319  df-0g 17490  df-mgm 18694  df-sgrp 18773  df-mnd 18789  df-mgp 20213  df-ur 20260  df-ring 20313

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  20589  isnzr2  20597  drnglidl1ne0  20598  isnzr2hash  20599  0ring01eq  20609  subrgid  20654  rrgnz  20785  isdomn3  20795  isdrng2  20823  isdrngd  20843  isdrngdOLD  20845  fidomndrnglem  20850  abv1z  20901  abvneg  20903  srng1  20930  issrngd  20932  orng0le1  20951  suborng  20953  lmod1cl  20984  lmodvsneg  21001  lmodsubvs  21013  lmodsubdi  21014  lmodsubdir  21015  lmodprop2d  21019  rmodislmod  21025  lssvnegcl  21051  prdslmodd  21064  lmodvsinv  21131  islmhm2  21133  lbsind2  21176  lspsneq  21220  lspexch  21227  lidl1el  21325  rsp1  21340  rhmqusnsg  21392  rngqiprng1elbas  21393  rngqiprngghmlem1  21394  rngqiprngimf  21404  rngqiprngimf1  21407  rng2idl1cntr  21412  rngqiprngfulem1  21418  rngqiprngfulem4  21421  rngqiprngfulem5  21422  rngqiprngu  21425  rhmpreimaprmidl  21444  qsnzr  21448  ssdifidlprm  21451  prmidlsubm  21452  lpi1  21460  mulgrhm  21592  chrcl  21639  chrid  21640  chrdvds  21641  chrcong  21642  dvdschrmulg  21643  zncyg  21663  frobrhm  21690  ofldchr  21691  zrhpsgnelbas  21709  uvcvvcl2  21903  uvcff  21906  lindfind2  21933  sraassab  21983  asclf  21996  asclghm  21997  ascl0  21999  ascl1  22000  asclmul1  22001  asclmul2  22002  ascldimul  22003  rnascl  22006  assamulgscmlem1  22014  asclmulg  22017  psrlmod  22074  psr1cl  22075  psrascl  22093  mvrf  22099  mplsubrg  22119  mplmon  22151  mplmonmul  22152  mplcoe1  22153  mplind  22186  evlslem1  22198  evlsmaprhm  22247  mhppwdeg  22278  psd1  22295  psdascl  22296  coe1pwmul  22405  coe1id  22419  ply1chr  22431  lply1binomsc  22436  evls1maprhm  22501  rhmmpl  22505  rhmply1vr1  22509  mamumat1cl  22561  mat1bas  22571  matsc  22572  mat0dimid  22590  mat1mhm  22606  dmatid  22617  scmatscmide  22629  scmatscmiddistr  22630  scmatmats  22633  scmatscm  22635  scmatid  22636  scmataddcl  22638  scmatsubcl  22639  scmatmulcl  22640  smatvscl  22646  scmatrhmcl  22650  scmatf1  22653  scmatmhm  22656  mat0scmat  22660  mat1scmat  22661  mdet0pr  22714  mdet1  22723  mdetunilem8  22741  mdetunilem9  22742  mdetuni0  22743  mdetmul  22745  m2detleiblem5  22747  m2detleiblem6  22748  maducoeval2  22762  maduf  22763  madutpos  22764  madugsum  22765  madulid  22767  minmar1marrep  22772  minmar1cl  22773  marep01ma  22782  smadiadetglem1  22793  smadiadetglem2  22794  matinv  22799  1pmatscmul  22824  1elcpmat  22837  mat2pmat1  22854  decpmatid  22892  idpm2idmp  22923  chmatcl  22950  chmatval  22951  chpmat1dlem  22957  chpmat1d  22958  chpdmatlem0  22959  chpdmatlem2  22961  chpdmatlem3  22962  chpidmat  22969  chmaidscmat  22970  cpmidgsumm2pm  22991  cpmidpmatlem2  22993  cpmidpmatlem3  22994  cpmadugsumlemB  22996  cpmadugsumfi  22999  cpmidgsum2  23001  chcoeffeqlem  23007  tlmtgp  24318  nrginvrcnlem  24813  clmvsubval  25233  cvsmuleqdivd  25258  cphsubrglem  25301  deg1pwle  26242  deg1pw  26243  ply1nz  26244  mon1pid  26276  ply1remlem  26287  dchrmulcl  27375  dchrinv  27387  dchrhash  27397  lgsqrlem1  27472  lgsqrlem2  27473  lgsqrlem3  27474  lgsqrlem4  27475  isarchiofld  33456  elrgspnlem2  33500  fracerl  33566  fracfld  33568  primefldgen1  33581  imaslmod  33612  dvdsruasso  33638  rhmquskerlem  33673  elrspunidl  33676  elrspunsn  33677  drngidl  33681  drngidlhash  33682  mxidlprm  33694  drng0mxidl  33699  qsdrngilem  33717  qsdrnglem2  33719  rsprprmprmidl  33753  rprmasso2  33757  rprmirredlem  33761  rprmdvdsprod  33765  1arithufdlem4  33778  ressasclcl  33802  coe1mon  33818  deg1vr  33823  psrmon  33880  psrmonmul  33881  rlmdim  33941  drngdimgt0  33949  extdg1id  33997  ply1annnr  34034  rtelextdg2lem  34057  submatminr1  34141  madjusmdetlem1  34158  zarcmplem  34212  zrhnm  34298  zrhchr  34305  zrhcntr  34310  qqh1  34316  qqhucn  34323  lflsub  39726  eqlkr  39758  eqlkr3  39760  lduallmodlem  39811  ldualvsubcl  39815  ldualvsubval  39816  dochfl1  42135  lcfrlem2  42202  lcdvsubval  42277  mapdpglem30  42361  hgmapval1  42552  hdmapglem5  42581  rhmzrhval  42624  aks6d1c1p6  42766  deg1gprod  42792  deg1pow  42793  aks5lem2  42839  unitscyglem5  42851  rnasclg  43156  ricdrng1  43181  fidomncyc  43188  rhmpsr  43200  evlsbagval  43203  0prjspnrel  43244  mendlmod  43801  idomodle  43803  mon1psubm  43811  deg1mhm  43812  lidldomn1  48878  smprngprmrng  48986  mgpsumn  49021  ply1sclrmsm  49042  evl1at1  49050  linc0scn0  49081  linc1  49083  islindeps2  49141  lmod1lem5  49149  asclelbasALT  49662