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

Theorem ringgrp 17785
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 2451 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2451 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2451 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2451 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isring 17784 . 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 1023 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444    e. wcel 1887   A.wral 2737   ` cfv 5582  (class class class)co 6290   Basecbs 15121   +g cplusg 15190   .rcmulr 15191   Mndcmnd 16535   Grpcgrp 16669  mulGrpcmgp 17723   Ringcrg 17780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-nul 4534
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293  df-ring 17782
This theorem is referenced by:  ringmnd  17789  ring0cl  17802  ringacl  17808  ringcom  17809  ringabl  17810  ringlz  17817  ringrz  17818  ringnegl  17822  rngnegr  17823  ringmneg1  17824  ringmneg2  17825  ringm2neg  17826  ringsubdi  17827  rngsubdir  17828  mulgass2  17829  ringlghm  17832  ringrghm  17833  prdsringd  17840  imasring  17847  opprring  17859  dvdsrneg  17882  dvdsr02  17884  unitnegcl  17909  irrednegb  17939  dfrhm2  17945  isrhmd  17957  idrhm  17959  pwsco1rhm  17966  pwsco2rhm  17967  kerf1hrm  17971  drnggrp  17983  subrgsubg  18014  cntzsubr  18040  pwsdiagrhm  18041  isabvd  18048  abvneg  18062  abvsubtri  18063  abvtrivd  18068  srng0  18088  idsrngd  18090  lmodfgrp  18100  lmod0vs  18124  lmodvsneg  18132  lmodsubvs  18144  lmodsubdi  18145  lmodsubdir  18146  lssvnegcl  18179  lmodvsinv  18259  sralmod  18410  issubrngd2  18412  lidlsubg  18438  2idlcpbl  18458  0ringnnzr  18493  asclghm  18562  psrlmod  18625  psrdi  18630  psrdir  18631  psrring  18635  mpllsslem  18659  mplsubrg  18664  mplcoe1  18689  mplind  18725  evlslem2  18735  evlslem1  18738  coe1z  18856  coe1subfv  18859  evl1subd  18930  evl1gsumd  18945  cnfld0  18992  cnfldneg  18994  cnfldsub  18996  cnsubglem  19017  zringgrp  19044  mulgrhm  19069  chrdvds  19099  chrcong  19100  zncyg  19119  cygznlem3  19140  zrhpsgnelbas  19162  ip2subdi  19211  matinvgcell  19460  mat0dim0  19492  mat1ghm  19508  dmatsubcl  19523  dmatsgrp  19524  scmataddcl  19541  scmatsubcl  19542  scmatsgrp  19544  scmatsgrp1  19547  scmatghm  19558  mdetralt  19633  mdetero  19635  mdetunilem6  19642  mdetunilem9  19645  mdetuni0  19646  m2detleiblem6  19651  cpmatinvcl  19741  cpmatsubgpmat  19744  mat2pmatghm  19754  pm2mpghm  19840  chmatcl  19852  chpmat0d  19858  chpmat1d  19860  chpdmatlem1  19862  chpdmatlem2  19863  chpscmat  19866  chpscmatgsumbin  19868  chpscmatgsummon  19869  chp0mat  19870  chpidmat  19871  chfacfisf  19878  chfacfscmulgsum  19884  chfacfpmmulgsum  19888  cayhamlem1  19890  cpmadugsumlemF  19900  cpmidgsum2  19903  trggrp  21186  tlmtgp  21210  abvmet  21590  nrgdsdi  21668  nrgdsdir  21669  tngnrg  21677  cnngp  21800  cnfldtgp  21901  cphsubrglem  22155  mdegldg  23015  mdeg0  23019  mdegaddle  23023  deg1add  23052  deg1suble  23056  deg1sub  23057  deg1sublt  23059  ply1nzb  23071  ply1divmo  23086  ply1divex  23087  r1pcl  23108  r1pid  23110  dvdsq1p  23111  dvdsr1p  23112  ply1remlem  23113  ply1rem  23114  ig1peu  23122  ig1peuOLD  23123  reefgim  23405  lgsqrlem1  24269  lgsqrlem2  24270  lgsqrlem3  24271  lgsqrlem4  24272  abvcxp  24453  efghgrpOLD  26101  dvrdir  28553  orngsqr  28567  ornglmulle  28568  orngrmulle  28569  ornglmullt  28570  orngrmullt  28571  orngmullt  28572  ofldchr  28577  suborng  28578  isarchiofld  28580  rhmopp  28582  reofld  28603  zrhchr  28780  lfl0  32631  lflsub  32633  lfl0f  32635  lfladdass  32639  lfladd0l  32640  lflnegcl  32641  lflnegl  32642  ldualvsubcl  32722  ldualvsubval  32723  lkrin  32730  erng0g  34561  lclkrlem2m  35087  lcfrlem2  35111  lcdvsubval  35186  mapdpglem30  35270  baerlem3lem1  35275  baerlem5alem1  35276  baerlem5blem1  35277  baerlem5blem2  35280  hdmapinvlem3  35491  hdmapinvlem4  35492  hdmapglem7b  35499  hbtlem5  35987  mendlmod  36059  subrgacs  36066  idomrootle  36069  c0rhm  39965  c0rnghm  39966  zrrnghm  39970  lidldomn1  39974  invginvrid  40205  evl1at0  40236  linply1  40238
  Copyright terms: Public domain W3C validator