MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringidcl Structured version   Unicode version

Theorem ringidcl 17789
Description: The unit 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  |-  B  =  ( Base `  R
)
ringidcl.u  |-  .1.  =  ( 1r `  R )
Assertion
Ref Expression
ringidcl  |-  ( R  e.  Ring  ->  .1.  e.  B )

Proof of Theorem ringidcl
StepHypRef Expression
1 eqid 2422 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21ringmgp 17774 . 2  |-  ( R  e.  Ring  ->  (mulGrp `  R )  e.  Mnd )
3 ringidcl.b . . . 4  |-  B  =  ( Base `  R
)
41, 3mgpbas 17717 . . 3  |-  B  =  ( Base `  (mulGrp `  R ) )
5 ringidcl.u . . . 4  |-  .1.  =  ( 1r `  R )
61, 5ringidval 17725 . . 3  |-  .1.  =  ( 0g `  (mulGrp `  R ) )
74, 6mndidcl 16542 . 2  |-  ( (mulGrp `  R )  e.  Mnd  ->  .1.  e.  B )
82, 7syl 17 1  |-  ( R  e.  Ring  ->  .1.  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1868   ` cfv 5598   Basecbs 15109   Mndcmnd 16523  mulGrpcmgp 17711   1rcur 17723   Ringcrg 17768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-om 6704  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-nn 10611  df-2 10669  df-ndx 15112  df-slot 15113  df-base 15114  df-sets 15115  df-plusg 15191  df-0g 15328  df-mgm 16476  df-sgrp 16515  df-mnd 16525  df-mgp 17712  df-ur 17724  df-ring 17770
This theorem is referenced by:  ringcom  17797  ringnegl  17810  rngnegr  17811  ringmneg1  17812  ringmneg2  17813  imasring  17835  opprring  17847  dvdsrid  17867  dvdsrneg  17870  1unit  17874  ringinvdv  17910  isdrng2  17973  isdrngd  17988  subrgid  17998  abv1z  18048  abvneg  18050  srng1  18075  issrngd  18077  lmod1cl  18106  lmodvsneg  18120  lmodsubvs  18132  lmodsubdi  18133  lmodsubdir  18134  lmodprop2d  18138  lssvnegcl  18167  prdslmodd  18180  lmodvsinv  18247  islmhm2  18249  lbsind2  18292  lspsneq  18333  lspexch  18340  lidl1el  18430  rsp1  18436  lpi1  18460  isnzr2  18475  isnzr2hash  18476  0ring01eq  18483  fidomndrnglem  18518  asclf  18549  asclghm  18550  asclmul1  18551  asclmul2  18552  asclrhm  18554  rnascl  18555  assamulgscmlem1  18560  psrlmod  18613  psr1cl  18614  mvrf  18636  mplsubrg  18652  mplmon  18675  mplmonmul  18676  mplcoe1  18677  mplind  18713  evlslem1  18726  coe1pwmul  18860  ply1scl0  18871  ply1scl1  18873  ply1idvr1  18874  lply1binomsc  18889  mulgrhm  19056  chrcl  19084  chrid  19085  chrdvds  19086  chrcong  19087  zncyg  19106  zrhpsgnelbas  19149  uvcvvcl2  19333  uvcff  19336  lindfind2  19363  mamumat1cl  19451  mat1bas  19461  matsc  19462  mat0dimid  19480  mat1mhm  19496  dmatid  19507  scmatscmide  19519  scmatscmiddistr  19520  scmatmats  19523  scmatscm  19525  scmatid  19526  scmataddcl  19528  scmatsubcl  19529  scmatmulcl  19530  smatvscl  19536  scmatrhmcl  19540  scmatf1  19543  scmatmhm  19546  mat0scmat  19550  mat1scmat  19551  mdet0pr  19604  mdet1  19613  mdetunilem8  19631  mdetunilem9  19632  mdetuni0  19633  mdetmul  19635  m2detleiblem5  19637  m2detleiblem6  19638  maducoeval2  19652  maduf  19653  madutpos  19654  madugsum  19655  madulid  19657  minmar1marrep  19662  minmar1cl  19663  marep01ma  19672  smadiadetglem1  19683  smadiadetglem2  19684  matinv  19689  1pmatscmul  19713  1elcpmat  19726  mat2pmat1  19743  decpmatid  19781  idpm2idmp  19812  chmatcl  19839  chmatval  19840  chpmat1dlem  19846  chpmat1d  19847  chpdmatlem0  19848  chpdmatlem2  19850  chpdmatlem3  19851  chpidmat  19858  chmaidscmat  19859  cpmidgsumm2pm  19880  cpmidpmatlem2  19882  cpmidpmatlem3  19883  cpmadugsumlemB  19885  cpmadugsumfi  19888  cpmidgsum2  19890  chcoeffeqlem  19896  tlmtgp  21197  nrginvrcnlem  21680  cvsmuleqdivd  22129  cphsubrglem  22142  deg1pwle  23055  deg1pw  23056  ply1nz  23057  ply1remlem  23100  dchrmulcl  24164  dchrinv  24176  dchrhash  24186  lgsqrlem1  24256  lgsqrlem2  24257  lgsqrlem3  24258  lgsqrlem4  24259  orng0le1  28571  ofldchr  28573  suborng  28574  isarchiofld  28576  elrhmunit  28579  submatminr1  28632  madjusmdetlem1  28649  zrhnm  28769  zrhchr  28776  qqh1  28785  qqhucn  28792  lflsub  32552  eqlkr  32584  eqlkr3  32586  lduallmodlem  32637  ldualvsubcl  32641  ldualvsubval  32642  dochfl1  34963  lcfrlem2  35030  lcdvsubval  35105  mapdpglem30  35189  hgmapval1  35383  hdmapglem5  35412  mendlmod  35979  idomodle  35990  isdomn3  36001  mon1pid  36002  mon1psubm  36003  deg1mhm  36004  lidldomn1  39193  mgpsumn  39419  ascl0  39443  ascl1  39444  ply1sclrmsm  39449  coe1id  39450  evl1at1  39458  linc0scn0  39490  linc1  39492  islindeps2  39550  lmod1lem5  39558
  Copyright terms: Public domain W3C validator