Theorem ringgrp 18913

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656   ∈ wcel 2164  ∀wral 3117  ‘cfv 6127  (class class class)co 6910  Basecbs 16229  +_gcplusg 16312  ._rcmulr 16313  Mndcmnd 17654  Grpcgrp 17783  mulGrpcmgp 18850  Ringcrg 18908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-nul 5015

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-iota 6090  df-fv 6135  df-ov 6913  df-ring 18910

This theorem is referenced by:  ringmnd  18917  ring0cl  18930  ringacl  18939  ringcom  18940  ringabl  18941  ringlz  18948  ringrz  18949  ringnegl  18955  rngnegr  18956  ringmneg1  18957  ringmneg2  18958  ringm2neg  18959  ringsubdi  18960  rngsubdir  18961  mulgass2  18962  ringlghm  18965  ringrghm  18966  prdsringd  18973  imasring  18980  opprring  18992  dvdsrneg  19015  dvdsr02  19017  unitnegcl  19042  irrednegb  19072  dfrhm2  19080  isrhmd  19092  idrhm  19094  pwsco1rhm  19101  pwsco2rhm  19102  kerf1hrm  19106  drnggrp  19118  subrgsubg  19149  cntzsubr  19175  pwsdiagrhm  19176  isabvd  19183  abvneg  19197  abvsubtri  19198  abvtrivd  19203  srng0  19223  idsrngd  19225  lmodfgrp  19235  lmod0vs  19259  lmodvsneg  19270  lmodsubvs  19282  lmodsubdi  19283  lmodsubdir  19284  rmodislmodlem  19293  rmodislmod  19294  lssvnegcl  19322  lmodvsinv  19402  sralmod  19555  issubrngd2  19557  lidlsubg  19583  2idlcpbl  19602  0ringnnzr  19637  asclghm  19706  psrlmod  19769  psrdi  19774  psrdir  19775  psrring  19779  mpllsslem  19803  mplsubrg  19808  mplcoe1  19833  mplind  19869  evlslem2  19879  evlslem1  19882  coe1z  20000  coe1subfv  20003  evl1subd  20073  evl1gsumd  20088  cnfld0  20137  cnfldneg  20139  cnfldsub  20141  cnsubglem  20162  zringgrp  20190  mulgrhm  20213  chrdvds  20243  chrcong  20244  zncyg  20263  cygznlem3  20284  zrhpsgnelbas  20307  ip2subdi  20358  matinvgcell  20615  mat0dim0  20648  mat1ghm  20664  dmatsubcl  20679  dmatsgrp  20680  scmataddcl  20697  scmatsubcl  20698  scmatsgrp  20700  scmatsgrp1  20703  scmatghm  20714  mdetralt  20789  mdetero  20791  mdetunilem6  20798  mdetunilem9  20801  mdetuni0  20802  m2detleiblem6  20807  cpmatinvcl  20899  cpmatsubgpmat  20902  mat2pmatghm  20912  pm2mpghm  20998  chmatcl  21010  chpmat0d  21016  chpmat1d  21018  chpdmatlem1  21020  chpdmatlem2  21021  chpscmat  21024  chpscmatgsumbin  21026  chpscmatgsummon  21027  chp0mat  21028  chpidmat  21029  chfacfisf  21036  chfacfscmulgsum  21042  chfacfpmmulgsum  21046  cayhamlem1  21048  cpmadugsumlemF  21058  cpmidgsum2  21061  trggrp  22352  tlmtgp  22376  abvmet  22757  nrgdsdi  22846  nrgdsdir  22847  tngnrg  22855  cnngp  22960  cnfldtgp  23049  cnncvsaddassdemo  23339  cphsubrglem  23353  mdegldg  24232  mdeg0  24236  mdegaddle  24240  deg1add  24269  deg1suble  24273  deg1sub  24274  deg1sublt  24276  ply1nzb  24288  ply1divmo  24301  ply1divex  24302  r1pcl  24323  r1pid  24325  dvdsq1p  24326  dvdsr1p  24327  ply1remlem  24328  ply1rem  24329  ig1peu  24337  reefgim  24610  lgsqrlem1  25491  lgsqrlem2  25492  lgsqrlem3  25493  lgsqrlem4  25494  abvcxp  25724  dvrdir  30331  orngsqr  30345  ornglmulle  30346  orngrmulle  30347  ornglmullt  30348  orngrmullt  30349  orngmullt  30350  ofldchr  30355  suborng  30356  isarchiofld  30358  rhmopp  30360  reofld  30381  zrhchr  30561  matunitlindflem1  33944  lfl0  35135  lflsub  35137  lfl0f  35139  lfladdass  35143  lfladd0l  35144  lflnegcl  35145  lflnegl  35146  ldualvsubcl  35226  ldualvsubval  35227  lkrin  35234  erng0g  37064  lclkrlem2m  37589  lcfrlem2  37613  lcdvsubval  37688  mapdpglem30  37772  baerlem3lem1  37777  baerlem5alem1  37778  baerlem5blem1  37779  baerlem5blem2  37782  hdmapinvlem3  37990  hdmapinvlem4  37991  hdmapglem7b  37998  hbtlem5  38536  mendlmod  38601  subrgacs  38608  idomrootle  38611  c0rhm  42773  c0rnghm  42774  zrrnghm  42778  lidldomn1  42782  invginvrid  43009  evl1at0  43040  linply1  43042