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

Theorem ringgrp 17778
Description: A ring is a group. (Contributed by NM, 15-Sep-2011.)
Assertion
Ref Expression
ringgrp  |-  ( R  e.  Ring  ->  R  e. 
Grp )

Proof of Theorem ringgrp
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2423 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2423 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2423 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2423 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isring 17777 . 2  |-  ( R  e.  Ring  <->  ( R  e. 
Grp  /\  (mulGrp `  R
)  e.  Mnd  /\  A. x  e.  ( Base `  R ) A. y  e.  ( Base `  R
) A. z  e.  ( Base `  R
) ( ( x ( .r `  R
) ( y ( +g  `  R ) z ) )  =  ( ( x ( .r `  R ) y ) ( +g  `  R ) ( x ( .r `  R
) z ) )  /\  ( ( x ( +g  `  R
) y ) ( .r `  R ) z )  =  ( ( x ( .r
`  R ) z ) ( +g  `  R
) ( y ( .r `  R ) z ) ) ) ) )
65simp1bi 1021 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1869   A.wral 2776   ` cfv 5599  (class class class)co 6303   Basecbs 15114   +g cplusg 15183   .rcmulr 15184   Mndcmnd 16528   Grpcgrp 16662  mulGrpcmgp 17716   Ringcrg 17773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-nul 4553
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-iota 5563  df-fv 5607  df-ov 6306  df-ring 17775
This theorem is referenced by:  ringmnd  17782  ring0cl  17795  ringacl  17801  ringcom  17802  ringabl  17803  ringlz  17810  ringrz  17811  ringnegl  17815  rngnegr  17816  ringmneg1  17817  ringmneg2  17818  ringm2neg  17819  ringsubdi  17820  rngsubdir  17821  mulgass2  17822  ringlghm  17825  ringrghm  17826  prdsringd  17833  imasring  17840  opprring  17852  dvdsrneg  17875  dvdsr02  17877  unitnegcl  17902  irrednegb  17932  dfrhm2  17938  isrhmd  17950  idrhm  17952  pwsco1rhm  17959  pwsco2rhm  17960  kerf1hrm  17964  drnggrp  17976  subrgsubg  18007  cntzsubr  18033  pwsdiagrhm  18034  isabvd  18041  abvneg  18055  abvsubtri  18056  abvtrivd  18061  srng0  18081  idsrngd  18083  lmodfgrp  18093  lmod0vs  18117  lmodvsneg  18125  lmodsubvs  18137  lmodsubdi  18138  lmodsubdir  18139  lssvnegcl  18172  lmodvsinv  18252  sralmod  18403  issubrngd2  18405  lidlsubg  18431  2idlcpbl  18451  0ringnnzr  18486  asclghm  18555  psrlmod  18618  psrdi  18623  psrdir  18624  psrring  18628  mpllsslem  18652  mplsubrg  18657  mplcoe1  18682  mplind  18718  evlslem2  18728  evlslem1  18731  coe1z  18849  coe1subfv  18852  evl1subd  18923  evl1gsumd  18938  cnfld0  18985  cnfldneg  18987  cnfldsub  18989  cnsubglem  19010  zringgrp  19036  mulgrhm  19061  chrdvds  19091  chrcong  19092  zncyg  19111  cygznlem3  19132  zrhpsgnelbas  19154  ip2subdi  19203  matinvgcell  19452  mat0dim0  19484  mat1ghm  19500  dmatsubcl  19515  dmatsgrp  19516  scmataddcl  19533  scmatsubcl  19534  scmatsgrp  19536  scmatsgrp1  19539  scmatghm  19550  mdetralt  19625  mdetero  19627  mdetunilem6  19634  mdetunilem9  19637  mdetuni0  19638  m2detleiblem6  19643  cpmatinvcl  19733  cpmatsubgpmat  19736  mat2pmatghm  19746  pm2mpghm  19832  chmatcl  19844  chpmat0d  19850  chpmat1d  19852  chpdmatlem1  19854  chpdmatlem2  19855  chpscmat  19858  chpscmatgsumbin  19860  chpscmatgsummon  19861  chp0mat  19862  chpidmat  19863  chfacfisf  19870  chfacfscmulgsum  19876  chfacfpmmulgsum  19880  cayhamlem1  19882  cpmadugsumlemF  19892  cpmidgsum2  19895  trggrp  21178  tlmtgp  21202  abvmet  21582  nrgdsdi  21660  nrgdsdir  21661  tngnrg  21669  cnngp  21792  cnfldtgp  21893  cphsubrglem  22147  mdegldg  23007  mdeg0  23011  mdegaddle  23015  deg1add  23044  deg1suble  23048  deg1sub  23049  deg1sublt  23051  ply1nzb  23063  ply1divmo  23078  ply1divex  23079  r1pcl  23100  r1pid  23102  dvdsq1p  23103  dvdsr1p  23104  ply1remlem  23105  ply1rem  23106  ig1peu  23114  ig1peuOLD  23115  reefgim  23397  lgsqrlem1  24261  lgsqrlem2  24262  lgsqrlem3  24263  lgsqrlem4  24264  abvcxp  24445  efghgrpOLD  26093  dvrdir  28555  orngsqr  28569  ornglmulle  28570  orngrmulle  28571  ornglmullt  28572  orngrmullt  28573  orngmullt  28574  ofldchr  28579  suborng  28580  isarchiofld  28582  rhmopp  28584  reofld  28605  zrhchr  28782  lfl0  32556  lflsub  32558  lfl0f  32560  lfladdass  32564  lfladd0l  32565  lflnegcl  32566  lflnegl  32567  ldualvsubcl  32647  ldualvsubval  32648  lkrin  32655  erng0g  34486  lclkrlem2m  35012  lcfrlem2  35036  lcdvsubval  35111  mapdpglem30  35195  baerlem3lem1  35200  baerlem5alem1  35201  baerlem5blem1  35202  baerlem5blem2  35205  hdmapinvlem3  35416  hdmapinvlem4  35417  hdmapglem7b  35424  hbtlem5  35913  mendlmod  35985  subrgacs  35992  idomrootle  35995  c0rhm  39216  c0rnghm  39217  zrrnghm  39221  lidldomn1  39225  invginvrid  39458  evl1at0  39489  linply1  39491
  Copyright terms: Public domain W3C validator