Theorem ringgrp 20444

Description: A ring is a group. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised 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 2761	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2761	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2761	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2761	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20443	. 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 2145  ∀wral 3077  ‘cfv 6531  (class class class)co 7412  Basecbs 17367  +_gcplusg 17408  ._rcmulr 17409  Mndcmnd 18903  Grpcgrp 19124  mulGrpcmgp 20340  Ringcrg 20439

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 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-ring 20441

This theorem is used by:  ringbn0  20448  ringgrpd  20449  ringmnd  20450  ring0cl  20476  ringacl  20487  ringabl  20490  ringnegl  20513  ringnegr  20514  ringmneg1  20515  ringmneg2  20516  mulgass2  20520  ringlghm  20523  ringrghm  20524  prdsringd  20530  imasring  20540  dvdsrneg  20580  dvdsr02  20582  unitnegcl  20607  dvrdir  20622  irrednegb  20641  dfrhm2  20684  isrhmd  20702  idrhm  20705  pwsco1rhm  20721  pwsco2rhm  20722  rhmopp  20739  0ringnnzr  20756  c0rhm  20766  c0rnghm  20767  zrrnghm  20768  subrgsubg  20809  cntzsubr  20838  pwsdiagrhm  20839  subrgacs  21037  isabvd  21049  abvneg  21063  abvsubtri  21064  abvtrivd  21069  srng0  21091  idsrngd  21093  orngsqr  21103  ornglmulle  21104  orngrmulle  21105  ornglmullt  21106  orngrmullt  21107  orngmullt  21108  suborng  21113  lmodfgrp  21124  lmod0vs  21150  lmodvsneg  21161  lmodsubvs  21173  lmodsubdi  21174  lmodsubdir  21175  rmodislmodlem  21184  rmodislmod  21185  lmodvsinv  21291  sralmod  21442  issubrgd  21444  lidlsubg  21482  qsidomlem1  21616  qsidomlem2  21617  qsnzr  21619  cnfld0  21682  cnfldneg  21684  cnfldsub  21686  cnsubglem  21702  zringgrp  21738  mulgrhm  21763  chrdvds  21812  chrcong  21813  dvdschrmulg  21814  zncyg  21834  cygznlem3  21855  freshmansdream  21860  zrhpsgnelbas  21880  ip2subdi  21930  asclghm  22170  psrlmod  22247  psrring  22257  mpllsslem  22287  mplsubrg  22292  mplcoe1  22326  mplind  22359  evlslem2  22368  coe1z  22562  coe1subfv  22565  evl1subd  22640  evl1gsumd  22655  matinvgcell  22730  mat0dim0  22762  mat1ghm  22778  dmatsubcl  22793  dmatsgrp  22794  scmataddcl  22811  scmatsubcl  22812  scmatsgrp  22814  scmatsgrp1  22817  scmatghm  22828  mdetralt  22903  mdetero  22905  mdetunilem6  22912  mdetunilem9  22915  mdetuni0  22916  m2detleiblem6  22921  matunitlindflem1  22974  cpmatinvcl  23015  cpmatsubgpmat  23018  mat2pmatghm  23028  pm2mpghm  23114  chmatcl  23126  chpmat0d  23132  chpmat1d  23134  chpdmatlem1  23136  chpdmatlem2  23137  chpscmat  23140  chpscmatgsumbin  23142  chpscmatgsummon  23143  chp0mat  23144  chpidmat  23145  chfacfisf  23152  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  cayhamlem1  23164  cpmadugsumlemF  23174  cpmidgsum2  23177  trggrp  24471  tlmtgp  24495  abvmet  24874  nrgdsdi  24964  nrgdsdir  24965  tngnrg  24973  cnngp  25078  cnfldtgp  25170  cnncvsaddassdemo  25464  cphsubrglem  25478  mdegldg  26364  mdeg0  26368  mdegaddle  26372  deg1add  26401  deg1suble  26405  deg1sub  26406  deg1sublt  26408  ply1nzb  26421  ply1divmo  26434  ply1divex  26435  r1pcl  26457  r1pid  26459  dvdsq1p  26461  dvdsr1p  26462  ply1remlem  26463  ply1rem  26464  idomrootle  26471  ig1peu  26473  reefgim  26759  lgsqrlem1  27655  lgsqrlem2  27656  lgsqrlem3  27657  lgsqrlem4  27658  abvcxp  27924  isarchiofld  33742  rmfsupp2  33780  reofld  33886  linds2eq  33918  mxidlprm  33977  zringfrac  34068  esplyind  34189  vietadeg1  34192  fedgmullem1  34243  ccfldsrarelvec  34285  zrhchr  34588  lfl0  40090  lflsub  40092  lfl0f  40094  lfladdass  40098  lfladd0l  40099  lflnegcl  40100  lflnegl  40101  ldualvsubcl  40181  ldualvsubval  40182  lkrin  40189  erng0g  42019  lclkrlem2m  42544  lcfrlem2  42568  lcdvsubval  42643  mapdpglem30  42727  baerlem3lem1  42732  baerlem5alem1  42733  baerlem5blem1  42734  baerlem5blem2  42737  hdmapinvlem3  42945  hdmapinvlem4  42946  hdmapglem7b  42953  aks6d1c6lem2  43189  aks6d1c6lem3  43190  aks6d1c6isolem2  43193  aks5lem3a  43207  aks5lem7  43218  hbtlem5  44088  mendlmod  44149  lidldomn1  49272  invginvrid  49423  evl1at0  49447  linply1  49449