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

Theorem ringgrp 18598
Description: A ring is a group. (Contributed by NM, 15-Sep-2011.)
Assertion
Ref Expression
ringgrp (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Proof of Theorem ringgrp
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2651 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2651 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
3 eqid 2651 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2651 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 18597 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp1bi 1096 1 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  wral 2941  cfv 5926  (class class class)co 6690  Basecbs 15904  +gcplusg 15988  .rcmulr 15989  Mndcmnd 17341  Grpcgrp 17469  mulGrpcmgp 18535  Ringcrg 18593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-ring 18595
This theorem is referenced by:  ringmnd  18602  ring0cl  18615  ringacl  18624  ringcom  18625  ringabl  18626  ringlz  18633  ringrz  18634  ringnegl  18640  rngnegr  18641  ringmneg1  18642  ringmneg2  18643  ringm2neg  18644  ringsubdi  18645  rngsubdir  18646  mulgass2  18647  ringlghm  18650  ringrghm  18651  prdsringd  18658  imasring  18665  opprring  18677  dvdsrneg  18700  dvdsr02  18702  unitnegcl  18727  irrednegb  18757  dfrhm2  18765  isrhmd  18777  idrhm  18779  pwsco1rhm  18786  pwsco2rhm  18787  kerf1hrm  18791  drnggrp  18803  subrgsubg  18834  cntzsubr  18860  pwsdiagrhm  18861  isabvd  18868  abvneg  18882  abvsubtri  18883  abvtrivd  18888  srng0  18908  idsrngd  18910  lmodfgrp  18920  lmod0vs  18944  lmodvsneg  18955  lmodsubvs  18967  lmodsubdi  18968  lmodsubdir  18969  rmodislmodlem  18978  rmodislmod  18979  lssvnegcl  19004  lmodvsinv  19084  sralmod  19235  issubrngd2  19237  lidlsubg  19263  2idlcpbl  19282  0ringnnzr  19317  asclghm  19386  psrlmod  19449  psrdi  19454  psrdir  19455  psrring  19459  mpllsslem  19483  mplsubrg  19488  mplcoe1  19513  mplind  19550  evlslem2  19560  evlslem1  19563  coe1z  19681  coe1subfv  19684  evl1subd  19754  evl1gsumd  19769  cnfld0  19818  cnfldneg  19820  cnfldsub  19822  cnsubglem  19843  zringgrp  19871  mulgrhm  19894  chrdvds  19924  chrcong  19925  zncyg  19945  cygznlem3  19966  zrhpsgnelbas  19988  ip2subdi  20037  matinvgcell  20289  mat0dim0  20321  mat1ghm  20337  dmatsubcl  20352  dmatsgrp  20353  scmataddcl  20370  scmatsubcl  20371  scmatsgrp  20373  scmatsgrp1  20376  scmatghm  20387  mdetralt  20462  mdetero  20464  mdetunilem6  20471  mdetunilem9  20474  mdetuni0  20475  m2detleiblem6  20480  cpmatinvcl  20570  cpmatsubgpmat  20573  mat2pmatghm  20583  pm2mpghm  20669  chmatcl  20681  chpmat0d  20687  chpmat1d  20689  chpdmatlem1  20691  chpdmatlem2  20692  chpscmat  20695  chpscmatgsumbin  20697  chpscmatgsummon  20698  chp0mat  20699  chpidmat  20700  chfacfisf  20707  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  cayhamlem1  20719  cpmadugsumlemF  20729  cpmidgsum2  20732  trggrp  22022  tlmtgp  22046  abvmet  22427  nrgdsdi  22516  nrgdsdir  22517  tngnrg  22525  cnngp  22630  cnfldtgp  22719  cnncvsaddassdemo  23009  cphsubrglem  23023  mdegldg  23871  mdeg0  23875  mdegaddle  23879  deg1add  23908  deg1suble  23912  deg1sub  23913  deg1sublt  23915  ply1nzb  23927  ply1divmo  23940  ply1divex  23941  r1pcl  23962  r1pid  23964  dvdsq1p  23965  dvdsr1p  23966  ply1remlem  23967  ply1rem  23968  ig1peu  23976  reefgim  24249  lgsqrlem1  25116  lgsqrlem2  25117  lgsqrlem3  25118  lgsqrlem4  25119  abvcxp  25349  dvrdir  29918  orngsqr  29932  ornglmulle  29933  orngrmulle  29934  ornglmullt  29935  orngrmullt  29936  orngmullt  29937  ofldchr  29942  suborng  29943  isarchiofld  29945  rhmopp  29947  reofld  29968  zrhchr  30148  matunitlindflem1  33535  lfl0  34670  lflsub  34672  lfl0f  34674  lfladdass  34678  lfladd0l  34679  lflnegcl  34680  lflnegl  34681  ldualvsubcl  34761  ldualvsubval  34762  lkrin  34769  erng0g  36599  lclkrlem2m  37125  lcfrlem2  37149  lcdvsubval  37224  mapdpglem30  37308  baerlem3lem1  37313  baerlem5alem1  37314  baerlem5blem1  37315  baerlem5blem2  37318  hdmapinvlem3  37529  hdmapinvlem4  37530  hdmapglem7b  37537  hbtlem5  38015  mendlmod  38080  subrgacs  38087  idomrootle  38090  c0rhm  42237  c0rnghm  42238  zrrnghm  42242  lidldomn1  42246  invginvrid  42473  evl1at0  42504  linply1  42506
  Copyright terms: Public domain W3C validator