Theorem ringgrp 20383

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 2762	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2762	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2762	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2762	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20382	. 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 3078  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  +_gcplusg 17348  ._rcmulr 17349  Mndcmnd 18842  Grpcgrp 19063  mulGrpcmgp 20279  Ringcrg 20378

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-ring 20380

This theorem is used by:  ringgrpd  20387  ringmnd  20388  ring0cl  20414  ringacl  20425  ringabl  20428  ringnegl  20450  ringnegr  20451  ringmneg1  20452  ringmneg2  20453  mulgass2  20457  ringlghm  20460  ringrghm  20461  prdsringd  20467  imasring  20477  dvdsrneg  20517  dvdsr02  20519  unitnegcl  20544  dvrdir  20559  irrednegb  20578  dfrhm2  20621  isrhmd  20639  idrhm  20642  pwsco1rhm  20658  pwsco2rhm  20659  rhmopp  20675  0ringnnzr  20692  c0rhm  20702  c0rnghm  20703  zrrnghm  20704  subrgsubg  20745  cntzsubr  20774  pwsdiagrhm  20775  subrgacs  20972  isabvd  20984  abvneg  20998  abvsubtri  20999  abvtrivd  21004  srng0  21026  idsrngd  21028  orngsqr  21038  ornglmulle  21039  orngrmulle  21040  ornglmullt  21041  orngrmullt  21042  orngmullt  21043  suborng  21048  lmodfgrp  21059  lmod0vs  21085  lmodvsneg  21096  lmodsubvs  21108  lmodsubdi  21109  lmodsubdir  21110  rmodislmodlem  21119  rmodislmod  21120  lmodvsinv  21226  sralmod  21377  issubrgd  21379  lidlsubg  21417  qsidomlem1  21549  qsidomlem2  21550  qsnzr  21552  cnfld0  21615  cnfldneg  21617  cnfldsub  21619  cnsubglem  21635  zringgrp  21671  mulgrhm  21696  chrdvds  21745  chrcong  21746  dvdschrmulg  21747  zncyg  21767  cygznlem3  21788  freshmansdream  21793  zrhpsgnelbas  21813  ip2subdi  21863  asclghm  22103  psrlmod  22180  psrring  22190  mpllsslem  22220  mplsubrg  22225  mplcoe1  22259  mplind  22292  evlslem2  22301  coe1z  22495  coe1subfv  22498  evl1subd  22573  evl1gsumd  22588  matinvgcell  22663  mat0dim0  22695  mat1ghm  22711  dmatsubcl  22726  dmatsgrp  22727  scmataddcl  22744  scmatsubcl  22745  scmatsgrp  22747  scmatsgrp1  22750  scmatghm  22761  mdetralt  22836  mdetero  22838  mdetunilem6  22845  mdetunilem9  22848  mdetuni0  22849  m2detleiblem6  22854  matunitlindflem1  22907  cpmatinvcl  22948  cpmatsubgpmat  22951  mat2pmatghm  22961  pm2mpghm  23047  chmatcl  23059  chpmat0d  23065  chpmat1d  23067  chpdmatlem1  23069  chpdmatlem2  23070  chpscmat  23073  chpscmatgsumbin  23075  chpscmatgsummon  23076  chp0mat  23077  chpidmat  23078  chfacfisf  23085  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  cayhamlem1  23097  cpmadugsumlemF  23107  cpmidgsum2  23110  trggrp  24404  tlmtgp  24428  abvmet  24807  nrgdsdi  24897  nrgdsdir  24898  tngnrg  24906  cnngp  25011  cnfldtgp  25103  cnncvsaddassdemo  25397  cphsubrglem  25411  mdegldg  26298  mdeg0  26302  mdegaddle  26306  deg1add  26335  deg1suble  26339  deg1sub  26340  deg1sublt  26342  ply1nzb  26355  ply1divmo  26368  ply1divex  26369  r1pcl  26391  r1pid  26393  dvdsq1p  26395  dvdsr1p  26396  ply1remlem  26397  ply1rem  26398  idomrootle  26405  ig1peu  26407  reefgim  26693  lgsqrlem1  27590  lgsqrlem2  27591  lgsqrlem3  27592  lgsqrlem4  27593  abvcxp  27859  isarchiofld  33647  rmfsupp2  33685  reofld  33791  linds2eq  33822  mxidlprm  33881  zringfrac  33972  esplyind  34093  vietadeg1  34096  fedgmullem1  34147  ccfldsrarelvec  34189  zrhchr  34492  lfl0  39946  lflsub  39948  lfl0f  39950  lfladdass  39954  lfladd0l  39955  lflnegcl  39956  lflnegl  39957  ldualvsubcl  40037  ldualvsubval  40038  lkrin  40045  erng0g  41875  lclkrlem2m  42400  lcfrlem2  42424  lcdvsubval  42499  mapdpglem30  42583  baerlem3lem1  42588  baerlem5alem1  42589  baerlem5blem1  42590  baerlem5blem2  42593  hdmapinvlem3  42801  hdmapinvlem4  42802  hdmapglem7b  42809  aks6d1c6lem2  43045  aks6d1c6lem3  43046  aks6d1c6isolem2  43049  aks5lem3a  43063  aks5lem7  43074  hbtlem5  43977  mendlmod  44038  lidldomn1  49154  invginvrid  49305  evl1at0  49329  linply1  49331