Theorem ringgrp 20173

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  ._rcmulr 17178  Mndcmnd 18659  Grpcgrp 18863  mulGrpcmgp 20075  Ringcrg 20168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-ring 20170

This theorem is referenced by:  ringgrpd  20177  ringmnd  20178  ring0cl  20202  ringacl  20213  ringabl  20216  ringnegl  20237  ringnegr  20238  ringmneg1  20239  ringmneg2  20240  mulgass2  20244  ringlghm  20247  ringrghm  20248  prdsringd  20256  imasring  20266  dvdsrneg  20306  dvdsr02  20308  unitnegcl  20333  dvrdir  20348  irrednegb  20367  dfrhm2  20410  isrhmd  20423  idrhm  20425  pwsco1rhm  20435  pwsco2rhm  20436  rhmopp  20442  0ringnnzr  20458  c0rhm  20467  c0rnghm  20468  zrrnghm  20469  subrgsubg  20510  cntzsubr  20539  pwsdiagrhm  20540  subrgacs  20733  isabvd  20745  abvneg  20759  abvsubtri  20760  abvtrivd  20765  srng0  20787  idsrngd  20789  orngsqr  20799  ornglmulle  20800  orngrmulle  20801  ornglmullt  20802  orngrmullt  20803  orngmullt  20804  suborng  20809  lmodfgrp  20820  lmod0vs  20846  lmodvsneg  20857  lmodsubvs  20869  lmodsubdi  20870  lmodsubdir  20871  rmodislmodlem  20880  rmodislmod  20881  lmodvsinv  20988  sralmod  21139  issubrgd  21141  lidlsubg  21178  cnfld0  21347  cnfldneg  21350  cnfldsub  21352  cnsubglem  21370  zringgrp  21407  mulgrhm  21432  chrdvds  21481  chrcong  21482  dvdschrmulg  21483  zncyg  21503  cygznlem3  21524  freshmansdream  21529  zrhpsgnelbas  21549  ip2subdi  21599  asclghm  21838  psrlmod  21915  psrring  21925  mpllsslem  21955  mplsubrg  21960  mplcoe1  21992  mplind  22025  evlslem2  22034  coe1z  22205  coe1subfv  22208  evl1subd  22286  evl1gsumd  22301  matinvgcell  22379  mat0dim0  22411  mat1ghm  22427  dmatsubcl  22442  dmatsgrp  22443  scmataddcl  22460  scmatsubcl  22461  scmatsgrp  22463  scmatsgrp1  22466  scmatghm  22477  mdetralt  22552  mdetero  22554  mdetunilem6  22561  mdetunilem9  22564  mdetuni0  22565  m2detleiblem6  22570  cpmatinvcl  22661  cpmatsubgpmat  22664  mat2pmatghm  22674  pm2mpghm  22760  chmatcl  22772  chpmat0d  22778  chpmat1d  22780  chpdmatlem1  22782  chpdmatlem2  22783  chpscmat  22786  chpscmatgsumbin  22788  chpscmatgsummon  22789  chp0mat  22790  chpidmat  22791  chfacfisf  22798  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  cayhamlem1  22810  cpmadugsumlemF  22820  cpmidgsum2  22823  trggrp  24116  tlmtgp  24140  abvmet  24519  nrgdsdi  24609  nrgdsdir  24610  tngnrg  24618  cnngp  24723  cnfldtgp  24816  cnncvsaddassdemo  25119  cphsubrglem  25133  mdegldg  26027  mdeg0  26031  mdegaddle  26035  deg1add  26064  deg1suble  26068  deg1sub  26069  deg1sublt  26071  ply1nzb  26084  ply1divmo  26097  ply1divex  26098  r1pcl  26120  r1pid  26122  dvdsq1p  26124  dvdsr1p  26125  ply1remlem  26126  ply1rem  26127  idomrootle  26134  ig1peu  26136  reefgim  26416  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  abvcxp  27582  isarchiofld  33281  rmfsupp2  33320  reofld  33424  linds2eq  33462  qsidomlem1  33533  qsidomlem2  33534  qsnzr  33536  mxidlprm  33551  zringfrac  33635  esplyind  33731  vietadeg1  33734  fedgmullem1  33786  ccfldsrarelvec  33828  zrhchr  34131  matunitlindflem1  37813  lfl0  39321  lflsub  39323  lfl0f  39325  lfladdass  39329  lfladd0l  39330  lflnegcl  39331  lflnegl  39332  ldualvsubcl  39412  ldualvsubval  39413  lkrin  39420  erng0g  41250  lclkrlem2m  41775  lcfrlem2  41799  lcdvsubval  41874  mapdpglem30  41958  baerlem3lem1  41963  baerlem5alem1  41964  baerlem5blem1  41965  baerlem5blem2  41968  hdmapinvlem3  42176  hdmapinvlem4  42177  hdmapglem7b  42184  aks6d1c6lem2  42421  aks6d1c6lem3  42422  aks6d1c6isolem2  42425  aks5lem3a  42439  aks5lem7  42450  hbtlem5  43366  mendlmod  43427  lidldomn1  48473  invginvrid  48609  evl1at0  48633  linply1  48635