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

Theorem ringgrp 17071
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 2441 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2441 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2441 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2441 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isring 17070 . 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 1010 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1381    e. wcel 1802   A.wral 2791   ` cfv 5574  (class class class)co 6277   Basecbs 14504   +g cplusg 14569   .rcmulr 14570   Mndcmnd 15788   Grpcgrp 15922  mulGrpcmgp 17009   Ringcrg 17066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-nul 4562
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280  df-ring 17068
This theorem is referenced by:  ringmnd  17075  ring0cl  17088  ringacl  17094  ringcom  17095  ringabl  17096  ringlz  17103  ringrz  17104  ringnegl  17108  rngnegr  17109  ringmneg1  17110  ringmneg2  17111  ringm2neg  17112  ringsubdi  17113  rngsubdir  17114  mulgass2  17115  ringlghm  17118  ringrghm  17119  prdsringd  17129  imasring  17136  opprring  17148  dvdsrneg  17171  dvdsr02  17173  unitnegcl  17198  irrednegb  17228  dfrhm2  17234  isrhmd  17246  idrhm  17248  pwsco1rhm  17255  pwsco2rhm  17256  kerf1hrm  17260  drnggrp  17272  subrgsubg  17303  cntzsubr  17329  pwsdiagrhm  17330  isabvd  17337  abvneg  17351  abvsubtri  17352  abvtrivd  17357  srng0  17377  idsrngd  17379  lmodfgrp  17389  lmod0vs  17413  lmodvsneg  17422  lmodsubvs  17434  lmodsubdi  17435  lmodsubdir  17436  lssvnegcl  17470  lmodvsinv  17550  sralmod  17701  issubrngd2  17703  lidlsubg  17730  2idlcpbl  17750  0ringnnzr  17785  asclghm  17855  psrlmod  17922  psrdi  17929  psrdir  17930  psrring  17934  mpllsslem  17962  mpllsslemOLD  17964  mplsubrg  17970  mplcoe1  17995  mplind  18035  evlslem2  18048  evlslem1  18052  coe1z  18172  coe1subfv  18175  evl1subd  18246  evl1gsumd  18261  cnfld0  18310  cnfldneg  18312  cnfldsub  18314  cnsubglem  18335  zringgrp  18361  mulgrhm  18399  mulgghm2OLD  18401  mulgrhmOLD  18402  chrdvds  18432  chrcong  18433  zncyg  18454  cygznlem3  18475  zrhpsgnelbas  18497  ip2subdi  18546  matinvgcell  18804  mat0dim0  18836  mat1ghm  18852  dmatsubcl  18867  dmatsgrp  18868  scmataddcl  18885  scmatsubcl  18886  scmatsgrp  18888  scmatsgrp1  18891  scmatghm  18902  mdetralt  18977  mdetero  18979  mdetunilem6  18986  mdetunilem9  18989  mdetuni0  18990  m2detleiblem6  18995  cpmatinvcl  19085  cpmatsubgpmat  19088  mat2pmatghm  19098  pm2mpghm  19184  chmatcl  19196  chpmat0d  19202  chpmat1d  19204  chpdmatlem1  19206  chpdmatlem2  19207  chpscmat  19210  chpscmatgsumbin  19212  chpscmatgsummon  19213  chp0mat  19214  chpidmat  19215  chfacfisf  19222  chfacfscmulgsum  19228  chfacfpmmulgsum  19232  cayhamlem1  19234  cpmadugsumlemF  19244  cpmidgsum2  19247  trggrp  20540  tlmtgp  20564  abvmet  20962  nrgdsdi  21040  nrgdsdir  21041  tngnrg  21049  cnngp  21153  cnfldtgp  21239  cphsubrglem  21490  mdegldg  22332  mdeg0  22336  mdegaddle  22340  deg1add  22370  deg1suble  22374  deg1sub  22375  deg1sublt  22377  ply1nzb  22389  ply1divmo  22402  ply1divex  22403  r1pcl  22424  r1pid  22426  dvdsq1p  22427  dvdsr1p  22428  ply1remlem  22429  ply1rem  22430  ig1peu  22438  reefgim  22710  lgsqrlem1  23481  lgsqrlem2  23482  lgsqrlem3  23483  lgsqrlem4  23484  abvcxp  23665  efghgrpOLD  25240  dvrdir  27646  orngsqr  27660  ornglmulle  27661  orngrmulle  27662  ornglmullt  27663  orngrmullt  27664  orngmullt  27665  ofldchr  27670  suborng  27671  isarchiofld  27673  rhmopp  27675  reofld  27696  zrhchr  27823  hbtlem5  31045  mendlmod  31111  subrgacs  31118  idomrootle  31121  lidldomn1  32427  invginvrid  32668  evl1at0  32701  linply1  32703  lfl0  34492  lflsub  34494  lfl0f  34496  lfladdass  34500  lfladd0l  34501  lflnegcl  34502  lflnegl  34503  ldualvsubcl  34583  ldualvsubval  34584  lkrin  34591  erng0g  36422  lclkrlem2m  36948  lcfrlem2  36972  lcdvsubval  37047  mapdpglem30  37131  baerlem3lem1  37136  baerlem5alem1  37137  baerlem5blem1  37138  baerlem5blem2  37141  hdmapinvlem3  37352  hdmapinvlem4  37353  hdmapglem7b  37360
  Copyright terms: Public domain W3C validator