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

Theorem crngring 18763
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 2813 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21iscrng 18759 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
32simplbi 487 1 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cfv 6104  CMndccmn 18397  mulGrpcmgp 18694  Ringcrg 18752  CRingccrg 18753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-iota 6067  df-fv 6112  df-cring 18755
This theorem is referenced by:  gsummgp0  18813  prdscrngd  18818  crngbinom  18826  dvdsunit  18868  unitmulclb  18870  unitabl  18873  idsrngd  19069  rmodislmod  19138  quscrng  19452  assa2ass  19534  sraassa  19537  rlmassa  19538  asclrhm  19554  assamulgscmlem2  19561  psrcrng  19625  psrassa  19626  mplcrng  19665  mplassa  19666  mplcoe2  19681  mplbas2  19682  mplmon2mul  19712  mplind  19713  evlslem2  19723  evlslem6  19724  evlslem3  19725  evlslem1  19726  evlseu  19727  evlsval2  19731  evlrhm  19736  evlsscasrng  19737  evlsca  19738  evlsvarsrng  19739  evlvar  19740  mpfind  19747  ply1crng  19779  ply1assa  19780  lply1binom  19887  lply1binomsc  19888  evls1rhmlem  19897  evls1gsumadd  19900  evls1gsummul  19901  evl1val  19904  evl1sca  19909  evl1scad  19910  evl1var  19911  evl1vard  19912  evls1var  19913  evls1scasrng  19914  evls1varsrng  19915  evl1subd  19917  evl1expd  19920  pf1const  19921  pf1id  19922  pf1ind  19930  evl1gsumdlem  19931  evl1gsumd  19932  evl1gsumadd  19933  evl1gsummul  19935  evl1varpw  19936  evl1scvarpw  19938  evl1scvarpwval  19939  evl1gsummon  19940  cnring  19979  zringring  20032  zring0  20039  znzrh2  20104  zncyg  20107  zndvds0  20109  znf1o  20110  zzngim  20111  znfld  20119  znchr  20121  znunit  20122  znrrg  20124  cygznlem3  20128  re0g  20170  mamuvs2  20426  matassa  20464  madetsumid  20482  madetsmelbas  20485  madetsmelbas2  20486  mat1dimcrng  20498  dmatcrng  20523  scmatcrng  20542  mdetleib2  20609  mdetf  20616  m1detdiag  20618  mdetdiaglem  20619  mdetdiag  20620  mdet1  20622  mdetrlin  20623  mdetrsca  20624  mdetrsca2  20625  mdetr0  20626  mdet0  20627  mdetrlin2  20628  mdetralt  20629  mdetero  20631  mdetmul  20644  maducoeval2  20661  maduf  20662  madutpos  20663  madugsum  20664  madurid  20665  madulid  20666  marep01ma  20682  smadiadetlem0  20683  smadiadetlem1a  20685  smadiadetlem3lem2  20689  smadiadetlem3  20690  smadiadetlem4  20691  smadiadet  20692  smadiadetglem1  20693  smadiadetglem2  20694  smadiadetg  20695  matinv  20699  matunit  20700  slesolinv  20702  slesolinvbi  20703  slesolex  20704  cramerimplem1  20705  cramerimplem1OLD  20706  cramerimplem2  20707  cramerimplem3  20708  cramerimp  20709  cramer  20714  mat2pmatmul  20753  mat2pmatmhm  20755  mat2pmatrhm  20756  mat2pmatlin  20757  m2cpmmhm  20767  m2cpmrhm  20768  m2pmfzgsumcl  20770  m2cpmrngiso  20780  monmatcollpw  20801  pmatcollpwlem  20802  pmatcollpw  20803  pmatcollpwfi  20804  pmatcollpw3fi1lem2  20809  pmatcollpwscmat  20813  monmat2matmon  20846  pm2mp  20847  chpmatply1  20854  chpmat1d  20858  chpdmat  20863  chpscmat  20864  chpscmatgsumbin  20866  chpscmatgsummon  20867  chp0mat  20868  chpidmat  20869  chmaidscmat  20870  chfacfscmulcl  20879  chfacfscmul0  20880  chfacfscmulgsum  20882  chfacfpmmulcl  20883  chfacfpmmul0  20884  chfacfpmmulgsum  20886  chfacfpmmulgsum2  20887  cayhamlem1  20888  cpmadurid  20889  cpmidgsumm2pm  20891  cpmidpmatlem2  20893  cpmidpmatlem3  20894  cpmadugsumlemB  20896  cpmadugsumlemC  20897  cpmadugsumlemF  20898  cpmadugsumfi  20899  cpmidgsum2  20901  cpmadumatpolylem1  20903  cpmadumatpolylem2  20904  cpmadumatpoly  20905  cayhamlem2  20906  chcoeffeqlem  20907  cayhamlem4  20910  cayleyhamilton0  20911  cayleyhamiltonALT  20913  cayleyhamilton1  20914  recvs  23162  fta1glem1  24145  fta1g  24147  fta1blem  24148  dchrelbas3  25183  dchrelbasd  25184  dchrzrh1  25189  dchrzrhmul  25191  dchrmulcl  25194  dchrn0  25195  dchrfi  25200  dchrghm  25201  dchrabs  25205  dchrinv  25206  dchrptlem1  25209  dchrptlem2  25210  dchrptlem3  25211  dchrsum2  25213  dchrhash  25216  sum2dchr  25219  lgsqrlem1  25291  lgsqrlem2  25292  lgsqrlem3  25293  lgsqrlem4  25294  lgsdchr  25300  lgseisenlem3  25322  lgseisenlem4  25323  dchrisum0flblem1  25417  dchrisum0re  25422  rdivmuldivd  30122  subofld  30147  mdetpmtr1  30220  mdetpmtr12  30222  madjusmdetlem1  30224  madjusmdetlem4  30227  mdetlap  30229  frlmpwfi  38170  isnumbasgrplem3  38177  mendlmod  38265  idomrootle  38275  idomodle  38276  2zrng0  42507  cznabel  42523  cznrng  42524  crhmsubc  42647  fldcat  42651  fldhmsubc  42653  crhmsubcALTV  42665  fldcatALTV  42669  fldhmsubcALTV  42671  mgpsumz  42710  mgpsumn  42711  evl1at0  42748  evl1at1  42749
  Copyright terms: Public domain W3C validator