Theorem ringgrp 19295

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ‘cfv 6324  (class class class)co 7135  Basecbs 16475  +_gcplusg 16557  ._rcmulr 16558  Mndcmnd 17903  Grpcgrp 18095  mulGrpcmgp 19232  Ringcrg 19290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-ring 19292

This theorem is referenced by:  ringgrpd  19299  ringmnd  19300  ring0cl  19315  ringacl  19324  ringcom  19325  ringabl  19326  ringlz  19333  ringrz  19334  ringnegl  19340  rngnegr  19341  ringmneg1  19342  ringmneg2  19343  ringm2neg  19344  ringsubdi  19345  rngsubdir  19346  mulgass2  19347  ringlghm  19350  ringrghm  19351  prdsringd  19358  imasring  19365  opprring  19377  dvdsrneg  19400  dvdsr02  19402  unitnegcl  19427  irrednegb  19457  dfrhm2  19465  isrhmd  19477  idrhm  19479  pwsco1rhm  19486  pwsco2rhm  19487  drnggrp  19503  subrgsubg  19534  cntzsubr  19561  pwsdiagrhm  19562  subrgacs  19572  isabvd  19584  abvneg  19598  abvsubtri  19599  abvtrivd  19604  srng0  19624  idsrngd  19626  lmodfgrp  19636  lmod0vs  19660  lmodvsneg  19671  lmodsubvs  19683  lmodsubdi  19684  lmodsubdir  19685  rmodislmodlem  19694  rmodislmod  19695  lssvnegcl  19721  lmodvsinv  19801  sralmod  19952  issubrngd2  19954  lidlsubg  19981  2idlcpbl  20000  0ringnnzr  20035  cnfld0  20115  cnfldneg  20117  cnfldsub  20119  cnsubglem  20140  zringgrp  20168  mulgrhm  20191  chrdvds  20220  chrcong  20221  zncyg  20240  cygznlem3  20261  zrhpsgnelbas  20283  ip2subdi  20333  asclghm  20569  psrlmod  20639  psrdi  20644  psrdir  20645  psrring  20649  mpllsslem  20673  mplsubrg  20678  mplcoe1  20705  mplind  20741  evlslem2  20751  evlslem1  20754  mhplss  20803  coe1z  20892  coe1subfv  20895  evl1subd  20966  evl1gsumd  20981  matinvgcell  21040  mat0dim0  21072  mat1ghm  21088  dmatsubcl  21103  dmatsgrp  21104  scmataddcl  21121  scmatsubcl  21122  scmatsgrp  21124  scmatsgrp1  21127  scmatghm  21138  mdetralt  21213  mdetero  21215  mdetunilem6  21222  mdetunilem9  21225  mdetuni0  21226  m2detleiblem6  21231  cpmatinvcl  21322  cpmatsubgpmat  21325  mat2pmatghm  21335  pm2mpghm  21421  chmatcl  21433  chpmat0d  21439  chpmat1d  21441  chpdmatlem1  21443  chpdmatlem2  21444  chpscmat  21447  chpscmatgsumbin  21449  chpscmatgsummon  21450  chp0mat  21451  chpidmat  21452  chfacfisf  21459  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  cayhamlem1  21471  cpmadugsumlemF  21481  cpmidgsum2  21484  trggrp  22777  tlmtgp  22801  abvmet  23182  nrgdsdi  23271  nrgdsdir  23272  tngnrg  23280  cnngp  23385  cnfldtgp  23474  cnncvsaddassdemo  23768  cphsubrglem  23782  mdegldg  24667  mdeg0  24671  mdegaddle  24675  deg1add  24704  deg1suble  24708  deg1sub  24709  deg1sublt  24711  ply1nzb  24723  ply1divmo  24736  ply1divex  24737  r1pcl  24758  r1pid  24760  dvdsq1p  24761  dvdsr1p  24762  ply1remlem  24763  ply1rem  24764  ig1peu  24772  reefgim  25045  lgsqrlem1  25930  lgsqrlem2  25931  lgsqrlem3  25932  lgsqrlem4  25933  abvcxp  26199  dvdschrmulg  30908  freshmansdream  30909  dvrdir  30912  rmfsupp2  30917  orngsqr  30928  ornglmulle  30929  orngrmulle  30930  ornglmullt  30931  orngrmullt  30932  orngmullt  30933  ofldchr  30938  suborng  30939  isarchiofld  30941  rhmopp  30943  reofld  30964  linds2eq  30995  qsidomlem1  31036  qsidomlem2  31037  mxidlprm  31048  fedgmullem1  31113  ccfldsrarelvec  31144  zrhchr  31327  matunitlindflem1  35053  lfl0  36361  lflsub  36363  lfl0f  36365  lfladdass  36369  lfladd0l  36370  lflnegcl  36371  lflnegl  36372  ldualvsubcl  36452  ldualvsubval  36453  lkrin  36460  erng0g  38290  lclkrlem2m  38815  lcfrlem2  38839  lcdvsubval  38914  mapdpglem30  38998  baerlem3lem1  39003  baerlem5alem1  39004  baerlem5blem1  39005  baerlem5blem2  39008  hdmapinvlem3  39216  hdmapinvlem4  39217  hdmapglem7b  39224  hbtlem5  40072  mendlmod  40137  idomrootle  40139  c0rhm  44536  c0rnghm  44537  zrrnghm  44541  lidldomn1  44545  invginvrid  44769  evl1at0  44799  linply1  44801