Theorem ringgrp 20351

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 2766	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2766	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2766	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2766	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20350	. 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 2146  ∀wral 3082  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  ._rcmulr 17336  Mndcmnd 18821  Grpcgrp 19031  mulGrpcmgp 20247  Ringcrg 20346

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-ring 20348

This theorem is used by:  ringgrpd  20355  ringmnd  20356  ring0cl  20382  ringacl  20393  ringabl  20396  ringnegl  20418  ringnegr  20419  ringmneg1  20420  ringmneg2  20421  mulgass2  20425  ringlghm  20428  ringrghm  20429  prdsringd  20435  imasring  20445  dvdsrneg  20485  dvdsr02  20487  unitnegcl  20512  dvrdir  20527  irrednegb  20546  dfrhm2  20589  isrhmd  20607  idrhm  20610  pwsco1rhm  20626  pwsco2rhm  20627  rhmopp  20643  0ringnnzr  20660  c0rhm  20670  c0rnghm  20671  zrrnghm  20672  subrgsubg  20713  cntzsubr  20742  pwsdiagrhm  20743  subrgacs  20940  isabvd  20952  abvneg  20966  abvsubtri  20967  abvtrivd  20972  srng0  20994  idsrngd  20996  orngsqr  21006  ornglmulle  21007  orngrmulle  21008  ornglmullt  21009  orngrmullt  21010  orngmullt  21011  suborng  21016  lmodfgrp  21027  lmod0vs  21053  lmodvsneg  21064  lmodsubvs  21076  lmodsubdi  21077  lmodsubdir  21078  rmodislmodlem  21087  rmodislmod  21088  lmodvsinv  21194  sralmod  21345  issubrgd  21347  lidlsubg  21385  qsidomlem1  21517  qsidomlem2  21518  qsnzr  21520  cnfld0  21583  cnfldneg  21585  cnfldsub  21587  cnsubglem  21603  zringgrp  21639  mulgrhm  21664  chrdvds  21713  chrcong  21714  dvdschrmulg  21715  zncyg  21735  cygznlem3  21756  freshmansdream  21761  zrhpsgnelbas  21781  ip2subdi  21831  asclghm  22069  psrlmod  22146  psrring  22156  mpllsslem  22186  mplsubrg  22191  mplcoe1  22225  mplind  22258  evlslem2  22267  coe1z  22461  coe1subfv  22464  evl1subd  22539  evl1gsumd  22554  matinvgcell  22629  mat0dim0  22661  mat1ghm  22677  dmatsubcl  22692  dmatsgrp  22693  scmataddcl  22710  scmatsubcl  22711  scmatsgrp  22713  scmatsgrp1  22716  scmatghm  22727  mdetralt  22802  mdetero  22804  mdetunilem6  22811  mdetunilem9  22814  mdetuni0  22815  m2detleiblem6  22820  cpmatinvcl  22911  cpmatsubgpmat  22914  mat2pmatghm  22924  pm2mpghm  23010  chmatcl  23022  chpmat0d  23028  chpmat1d  23030  chpdmatlem1  23032  chpdmatlem2  23033  chpscmat  23036  chpscmatgsumbin  23038  chpscmatgsummon  23039  chp0mat  23040  chpidmat  23041  chfacfisf  23048  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  cayhamlem1  23060  cpmadugsumlemF  23070  cpmidgsum2  23073  trggrp  24366  tlmtgp  24390  abvmet  24769  nrgdsdi  24859  nrgdsdir  24860  tngnrg  24868  cnngp  24973  cnfldtgp  25065  cnncvsaddassdemo  25359  cphsubrglem  25373  mdegldg  26260  mdeg0  26264  mdegaddle  26268  deg1add  26297  deg1suble  26301  deg1sub  26302  deg1sublt  26304  ply1nzb  26317  ply1divmo  26330  ply1divex  26331  r1pcl  26353  r1pid  26355  dvdsq1p  26357  dvdsr1p  26358  ply1remlem  26359  ply1rem  26360  idomrootle  26367  ig1peu  26369  reefgim  26650  lgsqrlem1  27547  lgsqrlem2  27548  lgsqrlem3  27549  lgsqrlem4  27550  abvcxp  27816  isarchiofld  33550  rmfsupp2  33588  reofld  33694  linds2eq  33725  mxidlprm  33784  zringfrac  33875  esplyind  33996  vietadeg1  33999  fedgmullem1  34050  ccfldsrarelvec  34092  zrhchr  34395  matunitlindflem1  38308  lfl0  39880  lflsub  39882  lfl0f  39884  lfladdass  39888  lfladd0l  39889  lflnegcl  39890  lflnegl  39891  ldualvsubcl  39971  ldualvsubval  39972  lkrin  39979  erng0g  41809  lclkrlem2m  42334  lcfrlem2  42358  lcdvsubval  42433  mapdpglem30  42517  baerlem3lem1  42522  baerlem5alem1  42523  baerlem5blem1  42524  baerlem5blem2  42527  hdmapinvlem3  42735  hdmapinvlem4  42736  hdmapglem7b  42743  aks6d1c6lem2  42979  aks6d1c6lem3  42980  aks6d1c6isolem2  42983  aks5lem3a  42997  aks5lem7  43008  hbtlem5  43896  mendlmod  43957  lidldomn1  49037  invginvrid  49188  evl1at0  49212  linply1  49214