Theorem ringgrp 20221

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099  ∀wral 3051  ‘cfv 6554  (class class class)co 7424  Basecbs 17213  +_gcplusg 17266  ._rcmulr 17267  Mndcmnd 18727  Grpcgrp 18928  mulGrpcmgp 20117  Ringcrg 20216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-nul 5311

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rab 3420  df-v 3464  df-sbc 3777  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562  df-ov 7427  df-ring 20218

This theorem is referenced by:  ringgrpd  20225  ringmnd  20226  ring0cl  20246  ringacl  20257  ringabl  20260  ringnegl  20281  ringnegr  20282  ringmneg1  20283  ringmneg2  20284  mulgass2  20288  ringlghm  20291  ringrghm  20292  prdsringd  20300  imasring  20309  dvdsrneg  20352  dvdsr02  20354  unitnegcl  20379  dvrdir  20394  irrednegb  20413  dfrhm2  20456  isrhmd  20470  idrhm  20472  pwsco1rhm  20484  pwsco2rhm  20485  rhmopp  20491  0ringnnzr  20507  c0rhm  20516  c0rnghm  20517  zrrnghm  20518  subrgsubg  20561  cntzsubr  20590  pwsdiagrhm  20591  subrgacs  20779  isabvd  20791  abvneg  20805  abvsubtri  20806  abvtrivd  20811  srng0  20833  idsrngd  20835  lmodfgrp  20845  lmod0vs  20871  lmodvsneg  20882  lmodsubvs  20894  lmodsubdi  20895  lmodsubdir  20896  rmodislmodlem  20905  rmodislmod  20906  rmodislmodOLD  20907  lmodvsinv  21014  sralmod  21173  issubrgd  21175  lidlsubg  21212  cnfld0  21384  cnfldneg  21387  cnfldsub  21389  cnsubglem  21412  zringgrp  21442  mulgrhm  21467  chrdvds  21520  chrcong  21521  dvdschrmulg  21522  zncyg  21546  cygznlem3  21567  freshmansdream  21572  zrhpsgnelbas  21590  ip2subdi  21640  asclghm  21880  psrlmod  21969  psrring  21979  mpllsslem  22009  mplsubrg  22014  mplcoe1  22044  mplind  22083  evlslem2  22094  coe1z  22254  coe1subfv  22257  evl1subd  22333  evl1gsumd  22348  matinvgcell  22428  mat0dim0  22460  mat1ghm  22476  dmatsubcl  22491  dmatsgrp  22492  scmataddcl  22509  scmatsubcl  22510  scmatsgrp  22512  scmatsgrp1  22515  scmatghm  22526  mdetralt  22601  mdetero  22603  mdetunilem6  22610  mdetunilem9  22613  mdetuni0  22614  m2detleiblem6  22619  cpmatinvcl  22710  cpmatsubgpmat  22713  mat2pmatghm  22723  pm2mpghm  22809  chmatcl  22821  chpmat0d  22827  chpmat1d  22829  chpdmatlem1  22831  chpdmatlem2  22832  chpscmat  22835  chpscmatgsumbin  22837  chpscmatgsummon  22838  chp0mat  22839  chpidmat  22840  chfacfisf  22847  chfacfscmulgsum  22853  chfacfpmmulgsum  22857  cayhamlem1  22859  cpmadugsumlemF  22869  cpmidgsum2  22872  trggrp  24167  tlmtgp  24191  abvmet  24575  nrgdsdi  24673  nrgdsdir  24674  tngnrg  24682  cnngp  24787  cnfldtgp  24878  cnncvsaddassdemo  25182  cphsubrglem  25196  mdegldg  26093  mdeg0  26097  mdegaddle  26101  deg1add  26130  deg1suble  26134  deg1sub  26135  deg1sublt  26137  ply1nzb  26150  ply1divmo  26163  ply1divex  26164  r1pcl  26186  r1pid  26188  dvdsq1p  26190  dvdsr1p  26191  ply1remlem  26192  ply1rem  26193  idomrootle  26200  ig1peu  26202  reefgim  26480  lgsqrlem1  27375  lgsqrlem2  27376  lgsqrlem3  27377  lgsqrlem4  27378  abvcxp  27644  rmfsupp2  33103  orngsqr  33182  ornglmulle  33183  orngrmulle  33184  ornglmullt  33185  orngrmullt  33186  orngmullt  33187  suborng  33193  isarchiofld  33195  reofld  33219  linds2eq  33256  qsidomlem1  33327  qsidomlem2  33328  qsnzr  33330  mxidlprm  33345  zringfrac  33429  fedgmullem1  33524  ccfldsrarelvec  33557  zrhchr  33791  matunitlindflem1  37317  lfl0  38763  lflsub  38765  lfl0f  38767  lfladdass  38771  lfladd0l  38772  lflnegcl  38773  lflnegl  38774  ldualvsubcl  38854  ldualvsubval  38855  lkrin  38862  erng0g  40693  lclkrlem2m  41218  lcfrlem2  41242  lcdvsubval  41317  mapdpglem30  41401  baerlem3lem1  41406  baerlem5alem1  41407  baerlem5blem1  41408  baerlem5blem2  41411  hdmapinvlem3  41619  hdmapinvlem4  41620  hdmapglem7b  41627  aks6d1c6lem2  41869  aks6d1c6lem3  41870  aks6d1c6isolem2  41873  aks5lem3a  41887  hbtlem5  42789  mendlmod  42854  lidldomn1  47608  invginvrid  47746  evl1at0  47774  linply1  47776

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »