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

Theorem ringgrp 17398
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 2454 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2454 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2454 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2454 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isring 17397 . 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 1009 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398    e. wcel 1823   A.wral 2804   ` cfv 5570  (class class class)co 6270   Basecbs 14716   +g cplusg 14784   .rcmulr 14785   Mndcmnd 16118   Grpcgrp 16252  mulGrpcmgp 17336   Ringcrg 17393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-ring 17395
This theorem is referenced by:  ringmnd  17402  ring0cl  17415  ringacl  17421  ringcom  17422  ringabl  17423  ringlz  17430  ringrz  17431  ringnegl  17435  rngnegr  17436  ringmneg1  17437  ringmneg2  17438  ringm2neg  17439  ringsubdi  17440  rngsubdir  17441  mulgass2  17442  ringlghm  17445  ringrghm  17446  prdsringd  17456  imasring  17463  opprring  17475  dvdsrneg  17498  dvdsr02  17500  unitnegcl  17525  irrednegb  17555  dfrhm2  17561  isrhmd  17573  idrhm  17575  pwsco1rhm  17582  pwsco2rhm  17583  kerf1hrm  17587  drnggrp  17599  subrgsubg  17630  cntzsubr  17656  pwsdiagrhm  17657  isabvd  17664  abvneg  17678  abvsubtri  17679  abvtrivd  17684  srng0  17704  idsrngd  17706  lmodfgrp  17716  lmod0vs  17740  lmodvsneg  17749  lmodsubvs  17761  lmodsubdi  17762  lmodsubdir  17763  lssvnegcl  17797  lmodvsinv  17877  sralmod  18028  issubrngd2  18030  lidlsubg  18057  2idlcpbl  18077  0ringnnzr  18112  asclghm  18182  psrlmod  18249  psrdi  18256  psrdir  18257  psrring  18261  mpllsslem  18289  mpllsslemOLD  18291  mplsubrg  18297  mplcoe1  18322  mplind  18362  evlslem2  18375  evlslem1  18379  coe1z  18499  coe1subfv  18502  evl1subd  18573  evl1gsumd  18588  cnfld0  18637  cnfldneg  18639  cnfldsub  18641  cnsubglem  18662  zringgrp  18688  mulgrhm  18710  chrdvds  18740  chrcong  18741  zncyg  18760  cygznlem3  18781  zrhpsgnelbas  18803  ip2subdi  18852  matinvgcell  19104  mat0dim0  19136  mat1ghm  19152  dmatsubcl  19167  dmatsgrp  19168  scmataddcl  19185  scmatsubcl  19186  scmatsgrp  19188  scmatsgrp1  19191  scmatghm  19202  mdetralt  19277  mdetero  19279  mdetunilem6  19286  mdetunilem9  19289  mdetuni0  19290  m2detleiblem6  19295  cpmatinvcl  19385  cpmatsubgpmat  19388  mat2pmatghm  19398  pm2mpghm  19484  chmatcl  19496  chpmat0d  19502  chpmat1d  19504  chpdmatlem1  19506  chpdmatlem2  19507  chpscmat  19510  chpscmatgsumbin  19512  chpscmatgsummon  19513  chp0mat  19514  chpidmat  19515  chfacfisf  19522  chfacfscmulgsum  19528  chfacfpmmulgsum  19532  cayhamlem1  19534  cpmadugsumlemF  19544  cpmidgsum2  19547  trggrp  20840  tlmtgp  20864  abvmet  21262  nrgdsdi  21340  nrgdsdir  21341  tngnrg  21349  cnngp  21453  cnfldtgp  21539  cphsubrglem  21790  mdegldg  22632  mdeg0  22636  mdegaddle  22640  deg1add  22670  deg1suble  22674  deg1sub  22675  deg1sublt  22677  ply1nzb  22689  ply1divmo  22702  ply1divex  22703  r1pcl  22724  r1pid  22726  dvdsq1p  22727  dvdsr1p  22728  ply1remlem  22729  ply1rem  22730  ig1peu  22738  reefgim  23011  lgsqrlem1  23814  lgsqrlem2  23815  lgsqrlem3  23816  lgsqrlem4  23817  abvcxp  23998  efghgrpOLD  25573  dvrdir  28015  orngsqr  28029  ornglmulle  28030  orngrmulle  28031  ornglmullt  28032  orngrmullt  28033  orngmullt  28034  ofldchr  28039  suborng  28040  isarchiofld  28042  rhmopp  28044  reofld  28065  zrhchr  28191  hbtlem5  31318  mendlmod  31383  subrgacs  31390  idomrootle  31393  c0rhm  32972  c0rnghm  32973  zrrnghm  32977  lidldomn1  32981  invginvrid  33214  evl1at0  33245  linply1  33247  lfl0  35187  lflsub  35189  lfl0f  35191  lfladdass  35195  lfladd0l  35196  lflnegcl  35197  lflnegl  35198  ldualvsubcl  35278  ldualvsubval  35279  lkrin  35286  erng0g  37117  lclkrlem2m  37643  lcfrlem2  37667  lcdvsubval  37742  mapdpglem30  37826  baerlem3lem1  37831  baerlem5alem1  37832  baerlem5blem1  37833  baerlem5blem2  37836  hdmapinvlem3  38047  hdmapinvlem4  38048  hdmapglem7b  38055
  Copyright terms: Public domain W3C validator