Theorem ringgrp 20497

Description: A ring is a group. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised 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.

Step	Hyp	Ref	Expression
1		eqid 2763	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2763	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2763	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2763	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20496	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1163	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ‘cfv 6561  (class class class)co 7446  Basecbs 17419  +_gcplusg 17460  ._rcmulr 17461  Mndcmnd 18955  Grpcgrp 19176  mulGrpcmgp 20393  Ringcrg 20492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-ring 20494

This theorem is used by:  ringbn0  20501  ringgrpd  20502  ringmnd  20503  ring0cl  20529  ringacl  20540  ringabl  20543  ringnegl  20566  ringnegr  20567  ringmneg1  20568  ringmneg2  20569  mulgass2  20573  ringlghm  20576  ringrghm  20577  prdsringd  20583  imasring  20593  dvdsrneg  20633  dvdsr02  20635  unitnegcl  20660  dvrdir  20675  irrednegb  20694  dfrhm2  20737  isrhmd  20755  idrhm  20758  pwsco1rhm  20774  pwsco2rhm  20775  rhmopp  20792  0ringnnzr  20809  c0rhm  20819  c0rnghm  20820  zrrnghm  20821  subrgsubg  20862  cntzsubr  20891  pwsdiagrhm  20892  subrgacs  21090  isabvd  21102  abvneg  21116  abvsubtri  21117  abvtrivd  21122  srng0  21144  idsrngd  21146  orngsqr  21156  ornglmulle  21157  orngrmulle  21158  ornglmullt  21159  orngrmullt  21160  orngmullt  21161  suborng  21166  lmodfgrp  21177  lmod0vs  21203  lmodvsneg  21214  lmodsubvs  21226  lmodsubdi  21227  lmodsubdir  21228  rmodislmodlem  21237  rmodislmod  21238  lmodvsinv  21344  sralmod  21495  issubrgd  21497  lidlsubg  21535  qsidomlem1  21669  qsidomlem2  21670  qsnzr  21672  cnfld0  21735  cnfldneg  21737  cnfldsub  21739  cnsubglem  21755  zringgrp  21791  mulgrhm  21816  chrdvds  21865  chrcong  21866  dvdschrmulg  21867  zncyg  21887  cygznlem3  21908  freshmansdream  21913  zrhpsgnelbas  21933  ip2subdi  21983  asclghm  22223  psrlmod  22300  mpllsslem  22340  mplsubrg  22345  mplcoe1  22379  mplind  22412  evlslem2  22421  coe1z  22615  coe1subfv  22618  evl1subd  22693  evl1gsumd  22708  matinvgcell  22783  mat0dim0  22815  mat1ghm  22831  dmatsubcl  22846  dmatsgrp  22847  scmataddcl  22864  scmatsubcl  22865  scmatsgrp  22867  scmatsgrp1  22870  scmatghm  22881  mdetralt  22956  mdetero  22958  mdetunilem6  22965  mdetunilem9  22968  mdetuni0  22969  m2detleiblem6  22974  matunitlindflem1  23027  cpmatinvcl  23068  cpmatsubgpmat  23071  mat2pmatghm  23081  pm2mpghm  23167  chmatcl  23179  chpmat0d  23185  chpmat1d  23187  chpdmatlem1  23189  chpdmatlem2  23190  chpscmat  23193  chpscmatgsumbin  23195  chpscmatgsummon  23196  chp0mat  23197  chpidmat  23198  chfacfisf  23205  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  cayhamlem1  23217  cpmadugsumlemF  23227  cpmidgsum2  23230  trggrp  24524  tlmtgp  24548  abvmet  24927  nrgdsdi  25017  nrgdsdir  25018  tngnrg  25026  cnngp  25131  cnfldtgp  25223  cnncvsaddassdemo  25517  cphsubrglem  25531  mdegldg  26417  mdeg0  26421  mdegaddle  26425  deg1add  26454  deg1suble  26458  deg1sub  26459  deg1sublt  26461  ply1nzb  26474  ply1divmo  26487  ply1divex  26488  r1pcl  26510  r1pid  26512  dvdsq1p  26514  dvdsr1p  26515  ply1remlem  26516  ply1rem  26517  idomrootle  26524  ig1peu  26526  reefgim  26810  lgsqrlem1  27706  lgsqrlem2  27707  lgsqrlem3  27708  lgsqrlem4  27709  abvcxp  27975  isarchiofld  33836  rmfsupp2  33874  reofld  33988  linds2eq  34020  mxidlprm  34079  zringfrac  34169  esplyind  34290  vietadeg1  34293  fedgmullem1  34344  ccfldsrarelvec  34386  zrhchr  34689  lfl0  40325  lflsub  40327  lfl0f  40329  lfladdass  40333  lfladd0l  40334  lflnegcl  40335  lflnegl  40336  ldualvsubcl  40416  ldualvsubval  40417  lkrin  40424  erng0g  42254  lclkrlem2m  42779  lcfrlem2  42803  lcdvsubval  42878  mapdpglem30  42962  baerlem3lem1  42967  baerlem5alem1  42968  baerlem5blem1  42969  baerlem5blem2  42972  hdmapinvlem3  43180  hdmapinvlem4  43181  hdmapglem7b  43188  aks6d1c6lem2  43424  aks6d1c6lem3  43425  aks6d1c6isolem2  43428  aks5lem3a  43442  aks5lem7  43453  hbtlem5  44333  mendlmod  44394  lidldomn1  49543  invginvrid  49694  evl1at0  49718  linply1  49720