Theorem ringgrp 18375

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Mndcmnd 17117  Grpcgrp 17245  mulGrpcmgp 18312  Ringcrg 18370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-ring 18372

This theorem is referenced by:  ringmnd  18379  ring0cl  18392  ringacl  18401  ringcom  18402  ringabl  18403  ringlz  18410  ringrz  18411  ringnegl  18417  rngnegr  18418  ringmneg1  18419  ringmneg2  18420  ringm2neg  18421  ringsubdi  18422  rngsubdir  18423  mulgass2  18424  ringlghm  18427  ringrghm  18428  prdsringd  18435  imasring  18442  opprring  18454  dvdsrneg  18477  dvdsr02  18479  unitnegcl  18504  irrednegb  18534  dfrhm2  18540  isrhmd  18552  idrhm  18554  pwsco1rhm  18561  pwsco2rhm  18562  kerf1hrm  18566  drnggrp  18578  subrgsubg  18609  cntzsubr  18635  pwsdiagrhm  18636  isabvd  18643  abvneg  18657  abvsubtri  18658  abvtrivd  18663  srng0  18683  idsrngd  18685  lmodfgrp  18695  lmod0vs  18719  lmodvsneg  18730  lmodsubvs  18742  lmodsubdi  18743  lmodsubdir  18744  lssvnegcl  18777  lmodvsinv  18857  sralmod  19008  issubrngd2  19010  lidlsubg  19036  2idlcpbl  19055  0ringnnzr  19090  asclghm  19159  psrlmod  19222  psrdi  19227  psrdir  19228  psrring  19232  mpllsslem  19256  mplsubrg  19261  mplcoe1  19286  mplind  19323  evlslem2  19333  evlslem1  19336  coe1z  19454  coe1subfv  19457  evl1subd  19527  evl1gsumd  19542  cnfld0  19589  cnfldneg  19591  cnfldsub  19593  cnsubglem  19614  zringgrp  19642  mulgrhm  19665  chrdvds  19695  chrcong  19696  zncyg  19716  cygznlem3  19737  zrhpsgnelbas  19759  ip2subdi  19808  matinvgcell  20060  mat0dim0  20092  mat1ghm  20108  dmatsubcl  20123  dmatsgrp  20124  scmataddcl  20141  scmatsubcl  20142  scmatsgrp  20144  scmatsgrp1  20147  scmatghm  20158  mdetralt  20233  mdetero  20235  mdetunilem6  20242  mdetunilem9  20245  mdetuni0  20246  m2detleiblem6  20251  cpmatinvcl  20341  cpmatsubgpmat  20344  mat2pmatghm  20354  pm2mpghm  20440  chmatcl  20452  chpmat0d  20458  chpmat1d  20460  chpdmatlem1  20462  chpdmatlem2  20463  chpscmat  20466  chpscmatgsumbin  20468  chpscmatgsummon  20469  chp0mat  20470  chpidmat  20471  chfacfisf  20478  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  cayhamlem1  20490  cpmadugsumlemF  20500  cpmidgsum2  20503  trggrp  21785  tlmtgp  21809  abvmet  22190  nrgdsdi  22279  nrgdsdir  22280  tngnrg  22288  cnngp  22393  cnfldtgp  22480  cnncvsaddassdemo  22771  cphsubrglem  22785  mdegldg  23630  mdeg0  23634  mdegaddle  23638  deg1add  23667  deg1suble  23671  deg1sub  23672  deg1sublt  23674  ply1nzb  23686  ply1divmo  23699  ply1divex  23700  r1pcl  23721  r1pid  23723  dvdsq1p  23724  dvdsr1p  23725  ply1remlem  23726  ply1rem  23727  ig1peu  23735  reefgim  24008  lgsqrlem1  24871  lgsqrlem2  24872  lgsqrlem3  24873  lgsqrlem4  24874  abvcxp  25104  dvrdir  29121  orngsqr  29135  ornglmulle  29136  orngrmulle  29137  ornglmullt  29138  orngrmullt  29139  orngmullt  29140  ofldchr  29145  suborng  29146  isarchiofld  29148  rhmopp  29150  reofld  29171  zrhchr  29348  matunitlindflem1  32575  lfl0  33370  lflsub  33372  lfl0f  33374  lfladdass  33378  lfladd0l  33379  lflnegcl  33380  lflnegl  33381  ldualvsubcl  33461  ldualvsubval  33462  lkrin  33469  erng0g  35300  lclkrlem2m  35826  lcfrlem2  35850  lcdvsubval  35925  mapdpglem30  36009  baerlem3lem1  36014  baerlem5alem1  36015  baerlem5blem1  36016  baerlem5blem2  36019  hdmapinvlem3  36230  hdmapinvlem4  36231  hdmapglem7b  36238  hbtlem5  36717  mendlmod  36782  subrgacs  36789  idomrootle  36792  c0rhm  41702  c0rnghm  41703  zrrnghm  41707  lidldomn1  41711  invginvrid  41942  evl1at0  41973  linply1  41975