Theorem ringgrp 20321

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.

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 20320	. 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)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  ._rcmulr 17312  Mndcmnd 18793  Grpcgrp 19001  mulGrpcmgp 20217  Ringcrg 20316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-ring 20318

This theorem is referenced by:  ringgrpd  20325  ringmnd  20326  ring0cl  20351  ringacl  20362  ringabl  20365  ringnegl  20386  ringnegr  20387  ringmneg1  20388  ringmneg2  20389  mulgass2  20393  ringlghm  20396  ringrghm  20397  prdsringd  20403  imasring  20413  dvdsrneg  20453  dvdsr02  20455  unitnegcl  20480  dvrdir  20495  irrednegb  20514  dfrhm2  20557  isrhmd  20571  idrhm  20573  pwsco1rhm  20585  pwsco2rhm  20586  rhmopp  20593  0ringnnzr  20610  c0rhm  20620  c0rnghm  20621  zrrnghm  20622  subrgsubg  20663  cntzsubr  20692  pwsdiagrhm  20693  subrgacs  20884  isabvd  20896  abvneg  20910  abvsubtri  20911  abvtrivd  20916  srng0  20938  idsrngd  20940  orngsqr  20950  ornglmulle  20951  orngrmulle  20952  ornglmullt  20953  orngrmullt  20954  orngmullt  20955  suborng  20960  lmodfgrp  20971  lmod0vs  20997  lmodvsneg  21008  lmodsubvs  21020  lmodsubdi  21021  lmodsubdir  21022  rmodislmodlem  21031  rmodislmod  21032  lmodvsinv  21138  sralmod  21289  issubrgd  21291  lidlsubg  21329  qsidomlem1  21461  qsidomlem2  21462  qsnzr  21464  cnfld0  21527  cnfldneg  21529  cnfldsub  21531  cnsubglem  21547  zringgrp  21583  mulgrhm  21608  chrdvds  21657  chrcong  21658  dvdschrmulg  21659  zncyg  21679  cygznlem3  21700  freshmansdream  21705  zrhpsgnelbas  21725  ip2subdi  21775  asclghm  22013  psrlmod  22090  psrring  22100  mpllsslem  22130  mplsubrg  22135  mplcoe1  22169  mplind  22202  evlslem2  22211  coe1z  22405  coe1subfv  22408  evl1subd  22483  evl1gsumd  22498  matinvgcell  22573  mat0dim0  22605  mat1ghm  22621  dmatsubcl  22636  dmatsgrp  22637  scmataddcl  22654  scmatsubcl  22655  scmatsgrp  22657  scmatsgrp1  22660  scmatghm  22671  mdetralt  22746  mdetero  22748  mdetunilem6  22755  mdetunilem9  22758  mdetuni0  22759  m2detleiblem6  22764  cpmatinvcl  22855  cpmatsubgpmat  22858  mat2pmatghm  22868  pm2mpghm  22954  chmatcl  22966  chpmat0d  22972  chpmat1d  22974  chpdmatlem1  22976  chpdmatlem2  22977  chpscmat  22980  chpscmatgsumbin  22982  chpscmatgsummon  22983  chp0mat  22984  chpidmat  22985  chfacfisf  22992  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  cayhamlem1  23004  cpmadugsumlemF  23014  cpmidgsum2  23017  trggrp  24310  tlmtgp  24334  abvmet  24713  nrgdsdi  24803  nrgdsdir  24804  tngnrg  24812  cnngp  24917  cnfldtgp  25009  cnncvsaddassdemo  25303  cphsubrglem  25317  mdegldg  26204  mdeg0  26208  mdegaddle  26212  deg1add  26241  deg1suble  26245  deg1sub  26246  deg1sublt  26248  ply1nzb  26261  ply1divmo  26274  ply1divex  26275  r1pcl  26297  r1pid  26299  dvdsq1p  26301  dvdsr1p  26302  ply1remlem  26303  ply1rem  26304  idomrootle  26311  ig1peu  26313  reefgim  26594  lgsqrlem1  27491  lgsqrlem2  27492  lgsqrlem3  27493  lgsqrlem4  27494  abvcxp  27760  isarchiofld  33500  rmfsupp2  33538  reofld  33644  linds2eq  33675  mxidlprm  33734  zringfrac  33825  esplyind  33946  vietadeg1  33949  fedgmullem1  34000  ccfldsrarelvec  34042  zrhchr  34345  matunitlindflem1  38248  lfl0  39820  lflsub  39822  lfl0f  39824  lfladdass  39828  lfladd0l  39829  lflnegcl  39830  lflnegl  39831  ldualvsubcl  39911  ldualvsubval  39912  lkrin  39919  erng0g  41749  lclkrlem2m  42274  lcfrlem2  42298  lcdvsubval  42373  mapdpglem30  42457  baerlem3lem1  42462  baerlem5alem1  42463  baerlem5blem1  42464  baerlem5blem2  42467  hdmapinvlem3  42675  hdmapinvlem4  42676  hdmapglem7b  42683  aks6d1c6lem2  42919  aks6d1c6lem3  42920  aks6d1c6isolem2  42923  aks5lem3a  42937  aks5lem7  42948  hbtlem5  43838  mendlmod  43899  lidldomn1  48979  invginvrid  49130  evl1at0  49154  linply1  49156