Theorem ringgrp 20256

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 2752	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2752	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2752	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2752	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20255	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1154	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1550   ∈ wcel 2132  ∀wral 3066  ‘cfv 6506  (class class class)co 7381  Basecbs 17217  +_gcplusg 17258  ._rcmulr 17259  Mndcmnd 18740  Grpcgrp 18947  mulGrpcmgp 20158  Ringcrg 20251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-nul 5246

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-ral 3067  df-rab 3405  df-v 3446  df-sbc 3736  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384  df-ring 20253

This theorem is referenced by:  ringgrpd  20260  ringmnd  20261  ring0cl  20285  ringacl  20296  ringabl  20299  ringnegl  20320  ringnegr  20321  ringmneg1  20322  ringmneg2  20323  mulgass2  20327  ringlghm  20330  ringrghm  20331  prdsringd  20337  imasring  20347  dvdsrneg  20387  dvdsr02  20389  unitnegcl  20414  dvrdir  20429  irrednegb  20448  dfrhm2  20491  isrhmd  20505  idrhm  20507  pwsco1rhm  20519  pwsco2rhm  20520  rhmopp  20527  0ringnnzr  20543  c0rhm  20552  c0rnghm  20553  zrrnghm  20554  subrgsubg  20595  cntzsubr  20624  pwsdiagrhm  20625  subrgacs  20818  isabvd  20830  abvneg  20844  abvsubtri  20845  abvtrivd  20850  srng0  20872  idsrngd  20874  orngsqr  20884  ornglmulle  20885  orngrmulle  20886  ornglmullt  20887  orngrmullt  20888  orngmullt  20889  suborng  20894  lmodfgrp  20905  lmod0vs  20931  lmodvsneg  20942  lmodsubvs  20954  lmodsubdi  20955  lmodsubdir  20956  rmodislmodlem  20965  rmodislmod  20966  lmodvsinv  21072  sralmod  21223  issubrgd  21225  lidlsubg  21262  cnfld0  21417  cnfldneg  21419  cnfldsub  21421  cnsubglem  21437  zringgrp  21473  mulgrhm  21498  chrdvds  21547  chrcong  21548  dvdschrmulg  21549  zncyg  21569  cygznlem3  21590  freshmansdream  21595  zrhpsgnelbas  21615  ip2subdi  21665  asclghm  21903  psrlmod  21980  psrring  21990  mpllsslem  22020  mplsubrg  22025  mplcoe1  22059  mplind  22092  evlslem2  22101  coe1z  22295  coe1subfv  22298  evl1subd  22374  evl1gsumd  22389  matinvgcell  22464  mat0dim0  22496  mat1ghm  22512  dmatsubcl  22527  dmatsgrp  22528  scmataddcl  22545  scmatsubcl  22546  scmatsgrp  22548  scmatsgrp1  22551  scmatghm  22562  mdetralt  22637  mdetero  22639  mdetunilem6  22646  mdetunilem9  22649  mdetuni0  22650  m2detleiblem6  22655  cpmatinvcl  22746  cpmatsubgpmat  22749  mat2pmatghm  22759  pm2mpghm  22845  chmatcl  22857  chpmat0d  22863  chpmat1d  22865  chpdmatlem1  22867  chpdmatlem2  22868  chpscmat  22871  chpscmatgsumbin  22873  chpscmatgsummon  22874  chp0mat  22875  chpidmat  22876  chfacfisf  22883  chfacfscmulgsum  22889  chfacfpmmulgsum  22893  cayhamlem1  22895  cpmadugsumlemF  22905  cpmidgsum2  22908  trggrp  24201  tlmtgp  24225  abvmet  24604  nrgdsdi  24694  nrgdsdir  24695  tngnrg  24703  cnngp  24808  cnfldtgp  24900  cnncvsaddassdemo  25194  cphsubrglem  25208  mdegldg  26095  mdeg0  26099  mdegaddle  26103  deg1add  26132  deg1suble  26136  deg1sub  26137  deg1sublt  26139  ply1nzb  26152  ply1divmo  26165  ply1divex  26166  r1pcl  26188  r1pid  26190  dvdsq1p  26192  dvdsr1p  26193  ply1remlem  26194  ply1rem  26195  idomrootle  26202  ig1peu  26204  reefgim  26479  lgsqrlem1  27376  lgsqrlem2  27377  lgsqrlem3  27378  lgsqrlem4  27379  abvcxp  27645  isarchiofld  33329  rmfsupp2  33368  reofld  33475  linds2eq  33513  qsidomlem1  33584  qsidomlem2  33585  qsnzr  33587  mxidlprm  33602  zringfrac  33694  esplyind  33816  vietadeg1  33819  fedgmullem1  33870  ccfldsrarelvec  33912  zrhchr  34215  matunitlindflem1  38053  lfl0  39627  lflsub  39629  lfl0f  39631  lfladdass  39635  lfladd0l  39636  lflnegcl  39637  lflnegl  39638  ldualvsubcl  39718  ldualvsubval  39719  lkrin  39726  erng0g  41556  lclkrlem2m  42081  lcfrlem2  42105  lcdvsubval  42180  mapdpglem30  42264  baerlem3lem1  42269  baerlem5alem1  42270  baerlem5blem1  42271  baerlem5blem2  42274  hdmapinvlem3  42482  hdmapinvlem4  42483  hdmapglem7b  42490  aks6d1c6lem2  42726  aks6d1c6lem3  42727  aks6d1c6isolem2  42730  aks5lem3a  42744  aks5lem7  42755  hbtlem5  43643  mendlmod  43704  lidldomn1  48791  invginvrid  48927  evl1at0  48951  linply1  48953