Theorem ringidcl 20003

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ‘cfv 6501  Basecbs 17094  Mndcmnd 18570  mulGrpcmgp 19910  1_rcur 19927  Ringcrg 19978

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 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137

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 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-nn 12163  df-2 12225  df-sets 17047  df-slot 17065  df-ndx 17077  df-base 17095  df-plusg 17160  df-0g 17337  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-mgp 19911  df-ur 19928  df-ring 19980

This theorem is referenced by:  ringid  20009  ringo2times  20010  ringadd2  20011  ringcomlem  20014  ringnegl  20032  ringnegr  20033  ringmneg1  20034  ringmneg2  20035  pwspjmhmmgpd  20057  imasring  20059  opprring  20074  dvdsrid  20094  dvdsrneg  20097  1unit  20101  ringinvdv  20139  elrhmunit  20199  isnzr2  20207  isnzr2hash  20208  0ring01eq  20214  isdrng2  20238  isdrngd  20255  isdrngdOLD  20257  subrgid  20272  abv1z  20347  abvneg  20349  srng1  20374  issrngd  20376  lmod1cl  20406  lmodvsneg  20423  lmodsubvs  20435  lmodsubdi  20436  lmodsubdir  20437  lmodprop2d  20441  rmodislmod  20447  rmodislmodOLD  20448  lssvnegcl  20474  prdslmodd  20487  lmodvsinv  20554  islmhm2  20556  lbsind2  20599  lspsneq  20642  lspexch  20649  lidl1el  20747  rsp1  20753  lpi1  20777  fidomndrnglem  20814  mulgrhm  20935  chrcl  20966  chrid  20967  chrdvds  20968  chrcong  20969  zncyg  20992  zrhpsgnelbas  21035  uvcvvcl2  21231  uvcff  21234  lindfind2  21261  asclf  21322  asclghm  21323  ascl0  21324  ascl1  21325  asclmul1  21326  asclmul2  21327  ascldimul  21328  rnascl  21331  assamulgscmlem1  21339  psrlmod  21407  psr1cl  21408  mvrf  21430  mplsubrg  21448  mplmon  21473  mplmonmul  21474  mplcoe1  21475  mplind  21515  evlslem1  21529  mhppwdeg  21577  coe1pwmul  21687  ply1scl0  21698  ply1scl1  21700  ply1idvr1  21701  lply1binomsc  21715  mamumat1cl  21825  mat1bas  21835  matsc  21836  mat0dimid  21854  mat1mhm  21870  dmatid  21881  scmatscmide  21893  scmatscmiddistr  21894  scmatmats  21897  scmatscm  21899  scmatid  21900  scmataddcl  21902  scmatsubcl  21903  scmatmulcl  21904  smatvscl  21910  scmatrhmcl  21914  scmatf1  21917  scmatmhm  21920  mat0scmat  21924  mat1scmat  21925  mdet0pr  21978  mdet1  21987  mdetunilem8  22005  mdetunilem9  22006  mdetuni0  22007  mdetmul  22009  m2detleiblem5  22011  m2detleiblem6  22012  maducoeval2  22026  maduf  22027  madutpos  22028  madugsum  22029  madulid  22031  minmar1marrep  22036  minmar1cl  22037  marep01ma  22046  smadiadetglem1  22057  smadiadetglem2  22058  matinv  22063  1pmatscmul  22088  1elcpmat  22101  mat2pmat1  22118  decpmatid  22156  idpm2idmp  22187  chmatcl  22214  chmatval  22215  chpmat1dlem  22221  chpmat1d  22222  chpdmatlem0  22223  chpdmatlem2  22225  chpdmatlem3  22226  chpidmat  22233  chmaidscmat  22234  cpmidgsumm2pm  22255  cpmidpmatlem2  22257  cpmidpmatlem3  22258  cpmadugsumlemB  22260  cpmadugsumfi  22263  cpmidgsum2  22265  chcoeffeqlem  22271  tlmtgp  23584  nrginvrcnlem  24092  clmvsubval  24509  cvsmuleqdivd  24534  cphsubrglem  24578  deg1pwle  25521  deg1pw  25522  ply1nz  25523  ply1remlem  25564  dchrmulcl  26634  dchrinv  26646  dchrhash  26656  lgsqrlem1  26731  lgsqrlem2  26732  lgsqrlem3  26733  lgsqrlem4  26734  dvdschrmulg  32136  frobrhm  32138  primefldgen1  32159  orng0le1  32178  ofldchr  32180  suborng  32181  isarchiofld  32183  imaslmod  32216  rhmqusker  32278  elrspunidl  32279  rhmpreimaprmidl  32300  mxidlprm  32313  asclmulg  32339  ply1chr  32360  coe1mon  32363  rgmoddim  32392  drngdimgt0  32400  extdg1id  32439  evls1maprhm  32455  submatminr1  32480  madjusmdetlem1  32497  zarcmplem  32551  zrhnm  32639  zrhchr  32646  qqh1  32655  qqhucn  32662  lflsub  37602  eqlkr  37634  eqlkr3  37636  lduallmodlem  37687  ldualvsubcl  37691  ldualvsubval  37692  dochfl1  40012  lcfrlem2  40079  lcdvsubval  40154  mapdpglem30  40238  hgmapval1  40429  hdmapglem5  40458  rnasclg  40742  ricdrng1  40778  rhmmpl  40799  evlsbagval  40806  mhphf  40829  0prjspnrel  41023  mendlmod  41578  idomodle  41581  isdomn3  41589  mon1pid  41590  mon1psubm  41591  deg1mhm  41592  lidldomn1  46339  mgpsumn  46559  ply1sclrmsm  46584  coe1id  46585  evl1at1  46593  linc0scn0  46624  linc1  46626  islindeps2  46684  lmod1lem5  46692