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

Theorem rngidcl 16655
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
rngidcl.b  |-  B  =  ( Base `  R
)
rngidcl.u  |-  .1.  =  ( 1r `  R )
Assertion
Ref Expression
rngidcl  |-  ( R  e.  Ring  ->  .1.  e.  B )

Proof of Theorem rngidcl
StepHypRef Expression
1 eqid 2438 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21rngmgp 16641 . 2  |-  ( R  e.  Ring  ->  (mulGrp `  R )  e.  Mnd )
3 rngidcl.b . . . 4  |-  B  =  ( Base `  R
)
41, 3mgpbas 16587 . . 3  |-  B  =  ( Base `  (mulGrp `  R ) )
5 rngidcl.u . . . 4  |-  .1.  =  ( 1r `  R )
61, 5rngidval 16595 . . 3  |-  .1.  =  ( 0g `  (mulGrp `  R ) )
74, 6mndidcl 15431 . 2  |-  ( (mulGrp `  R )  e.  Mnd  ->  .1.  e.  B )
82, 7syl 16 1  |-  ( R  e.  Ring  ->  .1.  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   ` cfv 5413   Basecbs 14166   Mndcmnd 15401  mulGrpcmgp 16581   1rcur 16593   Ringcrg 16635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-recs 6824  df-rdg 6858  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-plusg 14243  df-0g 14372  df-mnd 15407  df-mgp 16582  df-ur 16594  df-rng 16637
This theorem is referenced by:  rngcom  16663  rngnegl  16675  rngnegr  16676  rngmneg1  16677  rngmneg2  16678  imasrng  16701  opprrng  16713  dvdsrid  16733  dvdsrneg  16736  1unit  16740  rnginvdv  16776  isdrng2  16822  isdrngd  16837  subrgid  16847  abv1z  16897  abvneg  16899  srng1  16924  issrngd  16926  lmod1cl  16955  lmodvsneg  16969  lmodsubvs  16981  lmodsubdi  16982  lmodsubdir  16983  lmodprop2d  16987  lssvnegcl  17017  prdslmodd  17030  lmodvsinv  17097  islmhm2  17099  lbsind2  17142  lspsneq  17183  lspexch  17190  lidl1el  17280  rsp1  17286  lpi1  17310  isnzr2  17325  fidomndrnglem  17358  asclf  17388  asclghm  17389  asclmul1  17390  asclmul2  17391  asclrhm  17392  rnascl  17393  psrlmod  17452  psr1cl  17453  mvrf  17477  mplsubrg  17499  mplmon  17522  mplmonmul  17523  mplcoe1  17524  mplind  17564  evlslem1  17581  coe1pwmul  17712  ply1scl0  17722  ply1scl1  17724  mulgrhm  17906  mulgrhmOLD  17909  chrcl  17937  chrid  17938  chrdvds  17939  chrcong  17940  zncyg  17961  zrhpsgnelbas  18004  uvcvvcl2  18193  uvcff  18196  lindfind2  18227  mamudiagcl  18282  mat1bas  18316  matsc  18321  mdet0pr  18383  mdet1  18388  mdetunilem8  18405  mdetunilem9  18406  mdetuni0  18407  mdetmul  18409  m2detleiblem5  18411  m2detleiblem6  18412  maducoeval2  18426  maduf  18427  madutpos  18428  madugsum  18429  madulid  18431  minmar1marrep  18436  minmar1cl  18437  marep01ma  18446  smadiadetglem1  18457  smadiadetglem2  18458  matinv  18463  tlmtgp  19750  nrginvrcnlem  20251  cvsmuleqdivd  20663  cphsubrglem  20676  deg1pwle  21571  deg1pw  21572  ply1nz  21573  ply1remlem  21614  dchrmulcl  22568  dchrinv  22580  dchrhash  22590  lgsqrlem1  22660  lgsqrlem2  22661  lgsqrlem3  22662  lgsqrlem4  22663  orng0le1  26248  ofldchr  26250  suborng  26251  isarchiofld  26253  elrhmunit  26256  zrhnm  26367  zrhchr  26374  qqh1  26383  qqhucn  26390  mendlmod  29521  idomodle  29532  isdomn3  29543  mon1pid  29544  mon1psubm  29545  deg1mhm  29546  mgpsumn  30730  isnzr2hash  30743  0rng01eq  30745  ascl0  30781  ascl1  30782  assamulgscmlem1  30786  ply1idvr1  30793  ply1sclrmsm  30795  coe1id  30799  evl1at1  30810  lply1binomsc  30812  mat0dimid  30824  dmatid  30834  scmatid  30842  linc0scn0  30888  linc1  30890  islindeps2  30948  lmod1lem5  30964  lflsub  32605  eqlkr  32637  eqlkr3  32639  lduallmodlem  32690  ldualvsubcl  32694  ldualvsubval  32695  dochfl1  35014  lcfrlem2  35081  lcdvsubval  35156  mapdpglem30  35240  hgmapval1  35434  hdmapglem5  35463
  Copyright terms: Public domain W3C validator