Theorem ringgrp 20185

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  ._rcmulr 17190  Mndcmnd 18671  Grpcgrp 18875  mulGrpcmgp 20087  Ringcrg 20180

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-ring 20182

This theorem is referenced by:  ringgrpd  20189  ringmnd  20190  ring0cl  20214  ringacl  20225  ringabl  20228  ringnegl  20249  ringnegr  20250  ringmneg1  20251  ringmneg2  20252  mulgass2  20256  ringlghm  20259  ringrghm  20260  prdsringd  20268  imasring  20278  dvdsrneg  20318  dvdsr02  20320  unitnegcl  20345  dvrdir  20360  irrednegb  20379  dfrhm2  20422  isrhmd  20435  idrhm  20437  pwsco1rhm  20447  pwsco2rhm  20448  rhmopp  20454  0ringnnzr  20470  c0rhm  20479  c0rnghm  20480  zrrnghm  20481  subrgsubg  20522  cntzsubr  20551  pwsdiagrhm  20552  subrgacs  20745  isabvd  20757  abvneg  20771  abvsubtri  20772  abvtrivd  20777  srng0  20799  idsrngd  20801  orngsqr  20811  ornglmulle  20812  orngrmulle  20813  ornglmullt  20814  orngrmullt  20815  orngmullt  20816  suborng  20821  lmodfgrp  20832  lmod0vs  20858  lmodvsneg  20869  lmodsubvs  20881  lmodsubdi  20882  lmodsubdir  20883  rmodislmodlem  20892  rmodislmod  20893  lmodvsinv  21000  sralmod  21151  issubrgd  21153  lidlsubg  21190  cnfld0  21359  cnfldneg  21362  cnfldsub  21364  cnsubglem  21382  zringgrp  21419  mulgrhm  21444  chrdvds  21493  chrcong  21494  dvdschrmulg  21495  zncyg  21515  cygznlem3  21536  freshmansdream  21541  zrhpsgnelbas  21561  ip2subdi  21611  asclghm  21850  psrlmod  21927  psrring  21937  mpllsslem  21967  mplsubrg  21972  mplcoe1  22004  mplind  22037  evlslem2  22046  coe1z  22217  coe1subfv  22220  evl1subd  22298  evl1gsumd  22313  matinvgcell  22391  mat0dim0  22423  mat1ghm  22439  dmatsubcl  22454  dmatsgrp  22455  scmataddcl  22472  scmatsubcl  22473  scmatsgrp  22475  scmatsgrp1  22478  scmatghm  22489  mdetralt  22564  mdetero  22566  mdetunilem6  22573  mdetunilem9  22576  mdetuni0  22577  m2detleiblem6  22582  cpmatinvcl  22673  cpmatsubgpmat  22676  mat2pmatghm  22686  pm2mpghm  22772  chmatcl  22784  chpmat0d  22790  chpmat1d  22792  chpdmatlem1  22794  chpdmatlem2  22795  chpscmat  22798  chpscmatgsumbin  22800  chpscmatgsummon  22801  chp0mat  22802  chpidmat  22803  chfacfisf  22810  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  cayhamlem1  22822  cpmadugsumlemF  22832  cpmidgsum2  22835  trggrp  24128  tlmtgp  24152  abvmet  24531  nrgdsdi  24621  nrgdsdir  24622  tngnrg  24630  cnngp  24735  cnfldtgp  24828  cnncvsaddassdemo  25131  cphsubrglem  25145  mdegldg  26039  mdeg0  26043  mdegaddle  26047  deg1add  26076  deg1suble  26080  deg1sub  26081  deg1sublt  26083  ply1nzb  26096  ply1divmo  26109  ply1divex  26110  r1pcl  26132  r1pid  26134  dvdsq1p  26136  dvdsr1p  26137  ply1remlem  26138  ply1rem  26139  idomrootle  26146  ig1peu  26148  reefgim  26428  lgsqrlem1  27325  lgsqrlem2  27326  lgsqrlem3  27327  lgsqrlem4  27328  abvcxp  27594  isarchiofld  33292  rmfsupp2  33331  reofld  33435  linds2eq  33473  qsidomlem1  33544  qsidomlem2  33545  qsnzr  33547  mxidlprm  33562  zringfrac  33646  esplyind  33751  vietadeg1  33754  fedgmullem1  33806  ccfldsrarelvec  33848  zrhchr  34151  matunitlindflem1  37861  lfl0  39435  lflsub  39437  lfl0f  39439  lfladdass  39443  lfladd0l  39444  lflnegcl  39445  lflnegl  39446  ldualvsubcl  39526  ldualvsubval  39527  lkrin  39534  erng0g  41364  lclkrlem2m  41889  lcfrlem2  41913  lcdvsubval  41988  mapdpglem30  42072  baerlem3lem1  42077  baerlem5alem1  42078  baerlem5blem1  42079  baerlem5blem2  42082  hdmapinvlem3  42290  hdmapinvlem4  42291  hdmapglem7b  42298  aks6d1c6lem2  42535  aks6d1c6lem3  42536  aks6d1c6isolem2  42539  aks5lem3a  42553  aks5lem7  42564  hbtlem5  43479  mendlmod  43540  lidldomn1  48585  invginvrid  48721  evl1at0  48745  linply1  48747