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

Theorem ringidcl 18768
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 𝐵 = (Base‘𝑅)
ringidcl.u 1 = (1r𝑅)
Assertion
Ref Expression
ringidcl (𝑅 ∈ Ring → 1𝐵)

Proof of Theorem ringidcl
StepHypRef Expression
1 eqid 2760 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21ringmgp 18753 . 2 (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3 ringidcl.b . . . 4 𝐵 = (Base‘𝑅)
41, 3mgpbas 18695 . . 3 𝐵 = (Base‘(mulGrp‘𝑅))
5 ringidcl.u . . . 4 1 = (1r𝑅)
61, 5ringidval 18703 . . 3 1 = (0g‘(mulGrp‘𝑅))
74, 6mndidcl 17509 . 2 ((mulGrp‘𝑅) ∈ Mnd → 1𝐵)
82, 7syl 17 1 (𝑅 ∈ Ring → 1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  cfv 6049  Basecbs 16059  Mndcmnd 17495  mulGrpcmgp 18689  1rcur 18701  Ringcrg 18747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-plusg 16156  df-0g 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mgp 18690  df-ur 18702  df-ring 18749
This theorem is referenced by:  ringid  18774  rngo2times  18776  ringcom  18779  ringnegl  18794  rngnegr  18795  ringmneg1  18796  ringmneg2  18797  imasring  18819  opprring  18831  dvdsrid  18851  dvdsrneg  18854  1unit  18858  ringinvdv  18894  isdrng2  18959  isdrngd  18974  subrgid  18984  abv1z  19034  abvneg  19036  srng1  19061  issrngd  19063  lmod1cl  19092  lmodvsneg  19109  lmodsubvs  19121  lmodsubdi  19122  lmodsubdir  19123  lmodprop2d  19127  rmodislmod  19133  lssvnegcl  19158  prdslmodd  19171  lmodvsinv  19238  islmhm2  19240  lbsind2  19283  lspsneq  19324  lspexch  19331  lidl1el  19420  rsp1  19426  lpi1  19450  isnzr2  19465  isnzr2hash  19466  0ring01eq  19473  fidomndrnglem  19508  asclf  19539  asclghm  19540  asclmul1  19541  asclmul2  19542  asclrhm  19544  rnascl  19545  assamulgscmlem1  19550  psrlmod  19603  psr1cl  19604  mvrf  19626  mplsubrg  19642  mplmon  19665  mplmonmul  19666  mplcoe1  19667  mplind  19704  evlslem1  19717  coe1pwmul  19851  ply1scl0  19862  ply1scl1  19864  ply1idvr1  19865  lply1binomsc  19879  mulgrhm  20048  chrcl  20076  chrid  20077  chrdvds  20078  chrcong  20079  zncyg  20099  zrhpsgnelbas  20142  uvcvvcl2  20329  uvcff  20332  lindfind2  20359  mamumat1cl  20447  mat1bas  20457  matsc  20458  mat0dimid  20476  mat1mhm  20492  dmatid  20503  scmatscmide  20515  scmatscmiddistr  20516  scmatmats  20519  scmatscm  20521  scmatid  20522  scmataddcl  20524  scmatsubcl  20525  scmatmulcl  20526  smatvscl  20532  scmatrhmcl  20536  scmatf1  20539  scmatmhm  20542  mat0scmat  20546  mat1scmat  20547  mdet0pr  20600  mdet1  20609  mdetunilem8  20627  mdetunilem9  20628  mdetuni0  20629  mdetmul  20631  m2detleiblem5  20633  m2detleiblem6  20634  maducoeval2  20648  maduf  20649  madutpos  20650  madugsum  20651  madulid  20653  minmar1marrep  20658  minmar1cl  20659  marep01ma  20668  smadiadetglem1  20679  smadiadetglem2  20680  matinv  20685  1pmatscmul  20709  1elcpmat  20722  mat2pmat1  20739  decpmatid  20777  idpm2idmp  20808  chmatcl  20835  chmatval  20836  chpmat1dlem  20842  chpmat1d  20843  chpdmatlem0  20844  chpdmatlem2  20846  chpdmatlem3  20847  chpidmat  20854  chmaidscmat  20855  cpmidgsumm2pm  20876  cpmidpmatlem2  20878  cpmidpmatlem3  20879  cpmadugsumlemB  20881  cpmadugsumfi  20884  cpmidgsum2  20886  chcoeffeqlem  20892  tlmtgp  22200  nrginvrcnlem  22696  clmvsubval  23109  cvsmuleqdivd  23134  cphsubrglem  23177  deg1pwle  24078  deg1pw  24079  ply1nz  24080  ply1remlem  24121  dchrmulcl  25173  dchrinv  25185  dchrhash  25195  lgsqrlem1  25270  lgsqrlem2  25271  lgsqrlem3  25272  lgsqrlem4  25273  orng0le1  30121  ofldchr  30123  suborng  30124  isarchiofld  30126  elrhmunit  30129  submatminr1  30185  madjusmdetlem1  30202  zrhnm  30322  zrhchr  30329  qqh1  30338  qqhucn  30345  lflsub  34857  eqlkr  34889  eqlkr3  34891  lduallmodlem  34942  ldualvsubcl  34946  ldualvsubval  34947  dochfl1  37267  lcfrlem2  37334  lcdvsubval  37409  mapdpglem30  37493  hgmapval1  37687  hdmapglem5  37716  mendlmod  38265  idomodle  38276  isdomn3  38284  mon1pid  38285  mon1psubm  38286  deg1mhm  38287  lidldomn1  42431  mgpsumn  42652  ascl0  42675  ascl1  42676  ply1sclrmsm  42681  coe1id  42682  evl1at1  42690  linc0scn0  42722  linc1  42724  islindeps2  42782  lmod1lem5  42790
  Copyright terms: Public domain W3C validator