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

Theorem crngring 18758
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 2760 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21iscrng 18754 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
32simplbi 478 1 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  cfv 6049  CMndccmn 18393  mulGrpcmgp 18689  Ringcrg 18747  CRingccrg 18748
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-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-cring 18750
This theorem is referenced by:  gsummgp0  18808  prdscrngd  18813  crngbinom  18821  dvdsunit  18863  unitmulclb  18865  unitabl  18868  idsrngd  19064  rmodislmod  19133  quscrng  19442  assa2ass  19524  sraassa  19527  rlmassa  19528  asclrhm  19544  assamulgscmlem2  19551  psrcrng  19615  psrassa  19616  mplcrng  19655  mplassa  19656  mplcoe2  19671  mplbas2  19672  mplmon2mul  19703  mplind  19704  evlslem2  19714  evlslem6  19715  evlslem3  19716  evlslem1  19717  evlseu  19718  evlsval2  19722  evlrhm  19727  evlsscasrng  19728  evlsca  19729  evlsvarsrng  19730  evlvar  19731  mpfind  19738  ply1crng  19770  ply1assa  19771  lply1binom  19878  lply1binomsc  19879  evls1rhmlem  19888  evls1gsumadd  19891  evls1gsummul  19892  evl1val  19895  evl1sca  19900  evl1scad  19901  evl1var  19902  evl1vard  19903  evls1var  19904  evls1scasrng  19905  evls1varsrng  19906  evl1subd  19908  evl1expd  19911  pf1const  19912  pf1id  19913  pf1ind  19921  evl1gsumdlem  19922  evl1gsumd  19923  evl1gsumadd  19924  evl1gsummul  19926  evl1varpw  19927  evl1scvarpw  19929  evl1scvarpwval  19930  evl1gsummon  19931  cnring  19970  zringring  20023  zring0  20030  znzrh2  20096  zncyg  20099  zndvds0  20101  znf1o  20102  zzngim  20103  znfld  20111  znchr  20113  znunit  20114  znrrg  20116  cygznlem3  20120  re0g  20160  mamuvs2  20414  matassa  20452  madetsumid  20469  madetsmelbas  20472  madetsmelbas2  20473  mat1dimcrng  20485  dmatcrng  20510  scmatcrng  20529  mdetleib2  20596  mdetf  20603  m1detdiag  20605  mdetdiaglem  20606  mdetdiag  20607  mdet1  20609  mdetrlin  20610  mdetrsca  20611  mdetrsca2  20612  mdetr0  20613  mdet0  20614  mdetrlin2  20615  mdetralt  20616  mdetero  20618  mdetmul  20631  maducoeval2  20648  maduf  20649  madutpos  20650  madugsum  20651  madurid  20652  madulid  20653  marep01ma  20668  smadiadetlem0  20669  smadiadetlem1a  20671  smadiadetlem3lem2  20675  smadiadetlem3  20676  smadiadetlem4  20677  smadiadet  20678  smadiadetglem1  20679  smadiadetglem2  20680  smadiadetg  20681  matinv  20685  matunit  20686  slesolinv  20688  slesolinvbi  20689  slesolex  20690  cramerimplem1  20691  cramerimplem2  20692  cramerimplem3  20693  cramerimp  20694  cramer  20699  mat2pmatmul  20738  mat2pmatmhm  20740  mat2pmatrhm  20741  mat2pmatlin  20742  m2cpmmhm  20752  m2cpmrhm  20753  m2pmfzgsumcl  20755  m2cpmrngiso  20765  monmatcollpw  20786  pmatcollpwlem  20787  pmatcollpw  20788  pmatcollpwfi  20789  pmatcollpw3fi1lem2  20794  pmatcollpwscmat  20798  monmat2matmon  20831  pm2mp  20832  chpmatply1  20839  chpmat1d  20843  chpdmat  20848  chpscmat  20849  chpscmatgsumbin  20851  chpscmatgsummon  20852  chp0mat  20853  chpidmat  20854  chmaidscmat  20855  chfacfscmulcl  20864  chfacfscmul0  20865  chfacfscmulgsum  20867  chfacfpmmulcl  20868  chfacfpmmul0  20869  chfacfpmmulgsum  20871  chfacfpmmulgsum2  20872  cayhamlem1  20873  cpmadurid  20874  cpmidgsumm2pm  20876  cpmidpmatlem2  20878  cpmidpmatlem3  20879  cpmadugsumlemB  20881  cpmadugsumlemC  20882  cpmadugsumlemF  20883  cpmadugsumfi  20884  cpmidgsum2  20886  cpmadumatpolylem1  20888  cpmadumatpolylem2  20889  cpmadumatpoly  20890  cayhamlem2  20891  chcoeffeqlem  20892  cayhamlem4  20895  cayleyhamilton0  20896  cayleyhamiltonALT  20898  cayleyhamilton1  20899  recvs  23146  fta1glem1  24124  fta1g  24126  fta1blem  24127  dchrelbas3  25162  dchrelbasd  25163  dchrzrh1  25168  dchrzrhmul  25170  dchrmulcl  25173  dchrn0  25174  dchrfi  25179  dchrghm  25180  dchrabs  25184  dchrinv  25185  dchrptlem1  25188  dchrptlem2  25189  dchrptlem3  25190  dchrsum2  25192  dchrhash  25195  sum2dchr  25198  lgsqrlem1  25270  lgsqrlem2  25271  lgsqrlem3  25272  lgsqrlem4  25273  lgsdchr  25279  lgseisenlem3  25301  lgseisenlem4  25302  dchrisum0flblem1  25396  dchrisum0re  25401  rdivmuldivd  30100  subofld  30125  mdetpmtr1  30198  mdetpmtr12  30200  madjusmdetlem1  30202  madjusmdetlem4  30205  mdetlap  30207  frlmpwfi  38170  isnumbasgrplem3  38177  mendlmod  38265  idomrootle  38275  idomodle  38276  2zrng0  42448  cznabel  42464  cznrng  42465  crhmsubc  42588  fldcat  42592  fldhmsubc  42594  crhmsubcALTV  42606  fldcatALTV  42610  fldhmsubcALTV  42612  mgpsumz  42651  mgpsumn  42652  evl1at0  42689  evl1at1  42690
  Copyright terms: Public domain W3C validator