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

Theorem rnggrp 15596
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 2387 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2387 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
3 eqid 2387 . . 3  |-  ( +g  `  R )  =  ( +g  `  R )
4 eqid 2387 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
51, 2, 3, 4isrng 15595 . 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 972 1  |-  ( R  e.  Ring  ->  R  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2649   ` cfv 5394  (class class class)co 6020   Basecbs 13396   +g cplusg 13456   .rcmulr 13457   Mndcmnd 14611   Grpcgrp 14612  mulGrpcmgp 15575   Ringcrg 15587
This theorem is referenced by:  rngmnd  15600  rng0cl  15612  rngacl  15618  rngcom  15619  rngabl  15620  rnglz  15627  rngrz  15628  rngnegl  15630  rngnegr  15631  rngmneg1  15632  rngmneg2  15633  rngm2neg  15634  rngsubdi  15635  rngsubdir  15636  mulgass2  15637  rnglghm  15638  rngrghm  15639  prdsrngd  15645  imasrng  15652  opprrng  15663  dvdsrneg  15686  dvdsr02  15688  unitnegcl  15713  irrednegb  15743  dfrhm2  15748  isrhmd  15757  pwsco1rhm  15760  pwsco2rhm  15761  drnggrp  15770  subrgsubg  15801  cntzsubr  15827  pwsdiagrhm  15828  isabvd  15835  abvneg  15849  abvsubtri  15850  abvtrivd  15855  srng0  15875  lmodfgrp  15886  lmod0vs  15910  lmodvsneg  15915  lmodsubvs  15927  lmodsubdi  15928  lmodsubdir  15929  lssvnegcl  15959  lmodvsinv  16039  sralmod  16185  issubrngd2  16189  lidlsubg  16213  2idlcpbl  16232  asclghm  16324  psrlmod  16392  psrdi  16397  psrdir  16398  psrrng  16401  mpllsslem  16426  mplsubrg  16430  mplcoe1  16455  mplind  16489  evlslem2  16495  coe1z  16583  coe1subfv  16586  cnfld0  16648  cnfldneg  16650  cnfldsub  16652  cnsubglem  16670  mulgghm2  16709  mulgrhm  16710  chrdvds  16732  chrcong  16733  zncyg  16752  cygznlem3  16773  ip2subdi  16798  trggrp  18122  tlmtgp  18146  abvmet  18494  nrgdsdi  18572  nrgdsdir  18573  tngnrg  18581  cnngp  18685  cnfldtgp  18770  cphsubrglem  19011  evlslem1  19803  evl1subd  19822  mdegldg  19856  mdeg0  19860  mdegaddle  19864  deg1add  19893  deg1suble  19897  deg1sub  19898  deg1sublt  19900  ply1nzb  19912  ply1divmo  19925  ply1divex  19926  r1pcl  19947  r1pid  19949  dvdsq1p  19950  dvdsr1p  19951  ply1remlem  19952  ply1rem  19953  ig1peu  19961  reefgim  20233  lgsqrlem1  20992  lgsqrlem2  20993  lgsqrlem3  20994  lgsqrlem4  20995  abvcxp  21176  dvrdir  24055  ofldsqr  24066  ofldaddlt  24067  ofldchr  24070  subofld  24071  rhmopp  24073  kerf1hrm  24078  zrhchr  24159  hbtlem5  27001  mendlmod  27170  subrgacs  27177  idomrootle  27180  lfl0  29180  lflsub  29182  lfl0f  29184  lfladdass  29188  lfladd0l  29189  lflnegcl  29190  lflnegl  29191  ldualvsubcl  29271  ldualvsubval  29272  lkrin  29279  erng0g  31108  lclkrlem2m  31634  lcfrlem2  31658  lcdvsubval  31733  mapdpglem30  31817  baerlem3lem1  31822  baerlem5alem1  31823  baerlem5blem1  31824  baerlem5blem2  31827  hdmapinvlem3  32038  hdmapinvlem4  32039  hdmapglem7b  32046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-nul 4279
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-rng 15590
  Copyright terms: Public domain W3C validator