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

Theorem crngring 18327
Description: A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
crngring (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Proof of Theorem crngring
StepHypRef Expression
1 eqid 2609 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21iscrng 18323 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
32simplbi 474 1 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cfv 5790  CMndccmn 17962  mulGrpcmgp 18258  Ringcrg 18316  CRingccrg 18317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-cring 18319
This theorem is referenced by:  gsummgp0  18377  prdscrngd  18382  crngbinom  18390  dvdsunit  18432  unitmulclb  18434  unitabl  18437  idsrngd  18631  quscrng  19007  assa2ass  19089  sraassa  19092  rlmassa  19093  asclrhm  19109  assamulgscmlem2  19116  psrcrng  19180  psrassa  19181  mplcrng  19220  mplassa  19221  mplcoe2  19236  mplbas2  19237  mplmon2mul  19268  mplind  19269  evlslem2  19279  evlslem6  19280  evlslem3  19281  evlslem1  19282  evlseu  19283  evlsval2  19287  evlrhm  19292  evlsscasrng  19293  evlsca  19294  evlsvarsrng  19295  evlvar  19296  mpfind  19303  ply1crng  19335  ply1assa  19336  lply1binom  19443  lply1binomsc  19444  evls1rhmlem  19453  evls1gsumadd  19456  evls1gsummul  19457  evl1val  19460  evl1sca  19465  evl1scad  19466  evl1var  19467  evl1vard  19468  evls1var  19469  evls1scasrng  19470  evls1varsrng  19471  evl1subd  19473  evl1expd  19476  pf1const  19477  pf1id  19478  pf1ind  19486  evl1gsumdlem  19487  evl1gsumd  19488  evl1gsumadd  19489  evl1gsummul  19491  evl1varpw  19492  evl1scvarpw  19494  evl1scvarpwval  19495  evl1gsummon  19496  cnring  19533  zringring  19586  zring0  19593  znzrh2  19658  zncyg  19661  zndvds0  19663  znf1o  19664  zzngim  19665  znfld  19673  znchr  19675  znunit  19676  znrrg  19678  cygznlem3  19682  re0g  19722  mamuvs2  19973  matassa  20011  madetsumid  20028  madetsmelbas  20031  madetsmelbas2  20032  mat1dimcrng  20044  dmatcrng  20069  scmatcrng  20088  mdetleib2  20155  mdetf  20162  m1detdiag  20164  mdetdiaglem  20165  mdetdiag  20166  mdet1  20168  mdetrlin  20169  mdetrsca  20170  mdetrsca2  20171  mdetr0  20172  mdet0  20173  mdetrlin2  20174  mdetralt  20175  mdetero  20177  mdetmul  20190  maducoeval2  20207  maduf  20208  madutpos  20209  madugsum  20210  madurid  20211  madulid  20212  marep01ma  20227  smadiadetlem0  20228  smadiadetlem1a  20230  smadiadetlem3lem2  20234  smadiadetlem3  20235  smadiadetlem4  20236  smadiadet  20237  smadiadetglem1  20238  smadiadetglem2  20239  smadiadetg  20240  matinv  20244  matunit  20245  slesolinv  20247  slesolinvbi  20248  slesolex  20249  cramerimplem1  20250  cramerimplem2  20251  cramerimplem3  20252  cramerimp  20253  cramer  20258  mat2pmatmul  20297  mat2pmatmhm  20299  mat2pmatrhm  20300  mat2pmatlin  20301  m2cpmmhm  20311  m2cpmrhm  20312  m2pmfzgsumcl  20314  m2cpmrngiso  20324  monmatcollpw  20345  pmatcollpwlem  20346  pmatcollpw  20347  pmatcollpwfi  20348  pmatcollpw3fi1lem2  20353  pmatcollpwscmat  20357  monmat2matmon  20390  pm2mp  20391  chpmatply1  20398  chpmat1d  20402  chpdmat  20407  chpscmat  20408  chpscmatgsumbin  20410  chpscmatgsummon  20411  chp0mat  20412  chpidmat  20413  chmaidscmat  20414  chfacfscmulcl  20423  chfacfscmul0  20424  chfacfscmulgsum  20426  chfacfpmmulcl  20427  chfacfpmmul0  20428  chfacfpmmulgsum  20430  chfacfpmmulgsum2  20431  cayhamlem1  20432  cpmadurid  20433  cpmidgsumm2pm  20435  cpmidpmatlem2  20437  cpmidpmatlem3  20438  cpmadugsumlemB  20440  cpmadugsumlemC  20441  cpmadugsumlemF  20442  cpmadugsumfi  20443  cpmidgsum2  20445  cpmadumatpolylem1  20447  cpmadumatpolylem2  20448  cpmadumatpoly  20449  cayhamlem2  20450  chcoeffeqlem  20451  cayhamlem4  20454  cayleyhamilton0  20455  cayleyhamiltonALT  20457  cayleyhamilton1  20458  fta1glem1  23646  fta1g  23648  fta1blem  23649  dchrelbas3  24680  dchrelbasd  24681  dchrzrh1  24686  dchrzrhmul  24688  dchrmulcl  24691  dchrn0  24692  dchrfi  24697  dchrghm  24698  dchrabs  24702  dchrinv  24703  dchrptlem1  24706  dchrptlem2  24707  dchrptlem3  24708  dchrsum2  24710  dchrhash  24713  sum2dchr  24716  lgsqrlem1  24788  lgsqrlem2  24789  lgsqrlem3  24790  lgsqrlem4  24791  lgsdchr  24797  lgseisenlem3  24819  lgseisenlem4  24820  dchrisum0flblem1  24914  dchrisum0re  24919  rdivmuldivd  28928  subofld  28953  mdetpmtr1  29023  mdetpmtr12  29025  madjusmdetlem1  29027  madjusmdetlem4  29030  mdetlap  29032  frlmpwfi  36482  isnumbasgrplem3  36490  mendlmod  36578  idomrootle  36588  idomodle  36589  2zrng0  41723  cznabel  41741  cznrng  41742  crhmsubc  41865  fldcat  41869  fldhmsubc  41871  crhmsubcALTV  41884  fldcatALTV  41888  fldhmsubcALTV  41890  mgpsumz  41929  mgpsumn  41930  evl1at0  41968  evl1at1  41969
  Copyright terms: Public domain W3C validator