Theorem ringgrp 20255

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∀wral 3058  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  +_gcplusg 17297  ._rcmulr 17298  Mndcmnd 18759  Grpcgrp 18963  mulGrpcmgp 20151  Ringcrg 20250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-ring 20252

This theorem is referenced by:  ringgrpd  20259  ringmnd  20260  ring0cl  20280  ringacl  20291  ringabl  20294  ringnegl  20315  ringnegr  20316  ringmneg1  20317  ringmneg2  20318  mulgass2  20322  ringlghm  20325  ringrghm  20326  prdsringd  20334  imasring  20343  dvdsrneg  20386  dvdsr02  20388  unitnegcl  20413  dvrdir  20428  irrednegb  20447  dfrhm2  20490  isrhmd  20504  idrhm  20506  pwsco1rhm  20518  pwsco2rhm  20519  rhmopp  20525  0ringnnzr  20541  c0rhm  20550  c0rnghm  20551  zrrnghm  20552  subrgsubg  20593  cntzsubr  20622  pwsdiagrhm  20623  subrgacs  20817  isabvd  20829  abvneg  20843  abvsubtri  20844  abvtrivd  20849  srng0  20871  idsrngd  20873  lmodfgrp  20883  lmod0vs  20909  lmodvsneg  20920  lmodsubvs  20932  lmodsubdi  20933  lmodsubdir  20934  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  lmodvsinv  21052  sralmod  21211  issubrgd  21213  lidlsubg  21250  cnfld0  21422  cnfldneg  21425  cnfldsub  21427  cnsubglem  21450  zringgrp  21480  mulgrhm  21505  chrdvds  21558  chrcong  21559  dvdschrmulg  21560  zncyg  21584  cygznlem3  21605  freshmansdream  21610  zrhpsgnelbas  21629  ip2subdi  21679  asclghm  21920  psrlmod  21997  psrring  22007  mpllsslem  22037  mplsubrg  22042  mplcoe1  22072  mplind  22111  evlslem2  22120  coe1z  22281  coe1subfv  22284  evl1subd  22361  evl1gsumd  22376  matinvgcell  22456  mat0dim0  22488  mat1ghm  22504  dmatsubcl  22519  dmatsgrp  22520  scmataddcl  22537  scmatsubcl  22538  scmatsgrp  22540  scmatsgrp1  22543  scmatghm  22554  mdetralt  22629  mdetero  22631  mdetunilem6  22638  mdetunilem9  22641  mdetuni0  22642  m2detleiblem6  22647  cpmatinvcl  22738  cpmatsubgpmat  22741  mat2pmatghm  22751  pm2mpghm  22837  chmatcl  22849  chpmat0d  22855  chpmat1d  22857  chpdmatlem1  22859  chpdmatlem2  22860  chpscmat  22863  chpscmatgsumbin  22865  chpscmatgsummon  22866  chp0mat  22867  chpidmat  22868  chfacfisf  22875  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  cayhamlem1  22887  cpmadugsumlemF  22897  cpmidgsum2  22900  trggrp  24195  tlmtgp  24219  abvmet  24603  nrgdsdi  24701  nrgdsdir  24702  tngnrg  24710  cnngp  24815  cnfldtgp  24906  cnncvsaddassdemo  25210  cphsubrglem  25224  mdegldg  26119  mdeg0  26123  mdegaddle  26127  deg1add  26156  deg1suble  26160  deg1sub  26161  deg1sublt  26163  ply1nzb  26176  ply1divmo  26189  ply1divex  26190  r1pcl  26212  r1pid  26214  dvdsq1p  26216  dvdsr1p  26217  ply1remlem  26218  ply1rem  26219  idomrootle  26226  ig1peu  26228  reefgim  26508  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  abvcxp  27673  rmfsupp2  33227  orngsqr  33313  ornglmulle  33314  orngrmulle  33315  ornglmullt  33316  orngrmullt  33317  orngmullt  33318  suborng  33324  isarchiofld  33326  reofld  33351  linds2eq  33388  qsidomlem1  33459  qsidomlem2  33460  qsnzr  33462  mxidlprm  33477  zringfrac  33561  fedgmullem1  33656  ccfldsrarelvec  33695  zrhchr  33936  matunitlindflem1  37602  lfl0  39046  lflsub  39048  lfl0f  39050  lfladdass  39054  lfladd0l  39055  lflnegcl  39056  lflnegl  39057  ldualvsubcl  39137  ldualvsubval  39138  lkrin  39145  erng0g  40976  lclkrlem2m  41501  lcfrlem2  41525  lcdvsubval  41600  mapdpglem30  41684  baerlem3lem1  41689  baerlem5alem1  41690  baerlem5blem1  41691  baerlem5blem2  41694  hdmapinvlem3  41902  hdmapinvlem4  41903  hdmapglem7b  41910  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6isolem2  42156  aks5lem3a  42170  aks5lem7  42181  hbtlem5  43116  mendlmod  43177  lidldomn1  48074  invginvrid  48211  evl1at0  48236  linply1  48238