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

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

Proof of Theorem rnggrp
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2467 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2467 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2467 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 16999 . 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 1011 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   A.wral 2814   ` cfv 5587  (class class class)co 6283   Basecbs 14489   +g cplusg 14554   .rcmulr 14555   Mndcmnd 15725   Grpcgrp 15726  mulGrpcmgp 16940   Ringcrg 16995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5550  df-fv 5595  df-ov 6286  df-rng 16997
This theorem is referenced by:  rngmnd  17004  rng0cl  17016  rngacl  17022  rngcom  17023  rngabl  17024  rnglz  17031  rngrz  17032  rngnegl  17036  rngnegr  17037  rngmneg1  17038  rngmneg2  17039  rngm2neg  17040  rngsubdi  17041  rngsubdir  17042  mulgass2  17043  rnglghm  17046  rngrghm  17047  prdsrngd  17057  imasrng  17064  opprrng  17076  dvdsrneg  17099  dvdsr02  17101  unitnegcl  17126  irrednegb  17156  dfrhm2  17162  isrhmd  17174  pwsco1rhm  17182  pwsco2rhm  17183  kerf1hrm  17187  drnggrp  17199  subrgsubg  17230  cntzsubr  17256  pwsdiagrhm  17257  isabvd  17264  abvneg  17278  abvsubtri  17279  abvtrivd  17284  srng0  17304  idsrngd  17306  lmodfgrp  17316  lmod0vs  17340  lmodvsneg  17349  lmodsubvs  17361  lmodsubdi  17362  lmodsubdir  17363  lssvnegcl  17397  lmodvsinv  17477  sralmod  17628  issubrngd2  17630  lidlsubg  17657  2idlcpbl  17676  0rngnnzr  17711  asclghm  17774  psrlmod  17841  psrdi  17848  psrdir  17849  psrrng  17853  mpllsslem  17881  mpllsslemOLD  17883  mplsubrg  17889  mplcoe1  17914  mplind  17954  evlslem2  17967  evlslem1  17971  coe1z  18091  coe1subfv  18094  evl1subd  18165  evl1gsumd  18180  cnfld0  18229  cnfldneg  18231  cnfldsub  18233  cnsubglem  18251  zringgrp  18277  mulgrhm  18315  mulgghm2OLD  18317  mulgrhmOLD  18318  chrdvds  18348  chrcong  18349  zncyg  18370  cygznlem3  18391  zrhpsgnelbas  18413  ip2subdi  18462  matinvgcell  18720  mat0dim0  18752  mat1ghm  18768  dmatsubcl  18783  dmatsgrp  18784  scmataddcl  18801  scmatsubcl  18802  scmatsgrp  18804  scmatsgrp1  18807  scmatghm  18818  mdetralt  18893  mdetero  18895  mdetunilem6  18902  mdetunilem9  18905  mdetuni0  18906  m2detleiblem6  18911  cpmatinvcl  19001  cpmatsubgpmat  19004  mat2pmatghm  19014  pm2mpghm  19100  chmatcl  19112  chpmat0d  19118  chpmat1d  19120  chpdmatlem1  19122  chpdmatlem2  19123  chpscmat  19126  chpscmatgsumbin  19128  chpscmatgsummon  19129  chp0mat  19130  chpidmat  19131  chfacfisf  19138  chfacfscmulgsum  19144  chfacfpmmulgsum  19148  cayhamlem1  19150  cpmadugsumlemF  19160  cpmidgsum2  19163  trggrp  20425  tlmtgp  20449  abvmet  20847  nrgdsdi  20925  nrgdsdir  20926  tngnrg  20934  cnngp  21038  cnfldtgp  21124  cphsubrglem  21375  mdegldg  22217  mdeg0  22221  mdegaddle  22225  deg1add  22255  deg1suble  22259  deg1sub  22260  deg1sublt  22262  ply1nzb  22274  ply1divmo  22287  ply1divex  22288  r1pcl  22309  r1pid  22311  dvdsq1p  22312  dvdsr1p  22313  ply1remlem  22314  ply1rem  22315  ig1peu  22323  reefgim  22595  lgsqrlem1  23360  lgsqrlem2  23361  lgsqrlem3  23362  lgsqrlem4  23363  abvcxp  23544  dvrdir  27459  orngsqr  27473  ornglmulle  27474  orngrmulle  27475  ornglmullt  27476  orngrmullt  27477  orngmullt  27478  ofldchr  27483  suborng  27484  isarchiofld  27486  rhmopp  27488  reofld  27509  zrhchr  27609  hbtlem5  30697  mendlmod  30763  subrgacs  30770  idomrootle  30773  invginvrid  32045  evl1at0  32081  linply1  32083  lfl0  33871  lflsub  33873  lfl0f  33875  lfladdass  33879  lfladd0l  33880  lflnegcl  33881  lflnegl  33882  ldualvsubcl  33962  ldualvsubval  33963  lkrin  33970  erng0g  35799  lclkrlem2m  36325  lcfrlem2  36349  lcdvsubval  36424  mapdpglem30  36508  baerlem3lem1  36513  baerlem5alem1  36514  baerlem5blem1  36515  baerlem5blem2  36518  hdmapinvlem3  36729  hdmapinvlem4  36730  hdmapglem7b  36737
  Copyright terms: Public domain W3C validator