Theorem ringmgp 20186

Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.)

Hypothesis

Ref	Expression
ringmgp.g	⊢ 𝐺 = (mulGrp‘𝑅)

Assertion

Ref	Expression
ringmgp	⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Proof of Theorem ringmgp

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2737	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2737	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2737	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20184	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp2bi 1147	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  ._rcmulr 17190  Mndcmnd 18671  Grpcgrp 18875  mulGrpcmgp 20087  Ringcrg 20180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-ring 20182

This theorem is referenced by:  mgpf  20195  ringcl  20197  iscrng2  20199  ringass  20200  ringideu  20201  ringidcl  20212  ringidmlem  20215  ringsrg  20244  pwspjmhmmgpd  20275  pwsexpg  20276  unitsubm  20334  dfrhm2  20422  isrhm2d  20434  idrhm  20437  pwsco1rhm  20447  pwsco2rhm  20448  c0rhm  20479  c0rnghm  20480  subrgcrng  20520  subrgsubm  20530  issubrg3  20545  cntzsubr  20551  pwsdiagrhm  20552  isdomn3  20660  subrgacs  20745  cnfldexp  21371  expmhm  21403  nn0srg  21404  rge0srg  21405  fermltlchr  21496  freshmansdream  21541  frobrhm  21542  assamulgscmlem2  21868  psrcrng  21939  mplcoe3  22005  mplcoe5lem  22006  mplcoe5  22007  evlsvvvallem  22058  evlsvvval  22060  evlsgsummul  22064  mhppwdeg  22105  psdpw  22125  ply1moncl  22225  coe1pwmul  22233  ply1coefsupp  22253  ply1coe  22254  gsummoncoe1  22264  lply1binomsc  22267  evls1gsummul  22281  evl1expd  22301  evl1gsummul  22316  evl1scvarpw  22319  evl1scvarpwval  22320  evl1gsummon  22321  evls1fpws  22325  rhmply1mon  22345  ringvcl  22356  mat1mhm  22440  scmatmhm  22490  m1detdiag  22553  mdetdiaglem  22554  m2detleiblem2  22584  mat2pmatmhm  22689  pmatcollpwscmatlem1  22745  mply1topmatcllem  22759  mply1topmatcl  22761  pm2mpghm  22772  pm2mpmhm  22776  monmat2matmon  22780  pm2mp  22781  chpscmatgsumbin  22800  chpscmatgsummon  22801  chfacfscmulcl  22813  chfacfscmul0  22814  chfacfpmmulcl  22817  chfacfpmmul0  22818  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  cayhamlem2  22840  cayhamlem4  22844  nrgtrg  24646  deg1pw  26094  idomrootle  26146  plypf1  26185  efsubm  26528  amgm  26969  wilthlem2  27047  wilthlem3  27048  dchrelbas3  27217  lgsqrlem2  27326  lgsqrlem3  27327  lgsqrlem4  27328  cntrcrng  33174  psgnid  33190  cnmsgn0g  33239  altgnsg  33242  ringm1expp1  33327  isunit3  33334  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrgspn  33339  0ringcring  33345  domnprodn0  33368  rrgsubm  33377  znfermltl  33458  unitprodclb  33481  ringlsmss  33487  rprmdvdspow  33625  1arithidomlem1  33627  1arithidom  33629  1arithufdlem2  33637  1arithufdlem3  33638  1arithufdlem4  33639  zringfrac  33646  ressply1evls1  33657  evl1deg1  33668  evl1deg2  33669  evl1deg3  33670  evls1monply1  33671  ply1coedeg  33681  gsummoncoe1fzo  33689  vietalem  33755  ply1degltdimlem  33799  ply1degltdim  33800  assarrginv  33813  evls1fldgencl  33847  extdgfialglem1  33869  extdgfialglem2  33870  rtelextdg2lem  33903  2sqr3minply  33957  cos9thpiminplylem6  33964  cos9thpiminply  33965  iistmd  34079  aks6d1c1p2  42473  aks6d1c1p3  42474  aks6d1c1p6  42478  evl1gprodd  42481  aks6d1c2lem3  42490  idomnnzpownz  42496  aks6d1c5lem3  42501  aks6d1c5lem2  42502  deg1pow  42505  aks6d1c6lem1  42534  aks6d1c6lem2  42535  aks5lem2  42551  aks5lem3a  42553  domnexpgn0cl  42887  abvexp  42896  fidomncyc  42899  evlsexpval  42922  evlselv  42939  mhphf  42949  hbtlem4  43477  mon1psubm  43550  amgm2d  44548  amgm3d  44549  amgm4d  44550  invginvrid  48721  ply1mulgsumlem4  48743  ply1mulgsum  48744  amgmw2d  50157