Theorem ringmgp 20142

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  ._rcmulr 17180  Mndcmnd 18626  Grpcgrp 18830  mulGrpcmgp 20043  Ringcrg 20136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-ring 20138

This theorem is referenced by:  mgpf  20151  ringcl  20153  iscrng2  20155  ringass  20156  ringideu  20157  ringidcl  20168  ringidmlem  20171  ringsrg  20200  pwspjmhmmgpd  20231  pwsexpg  20232  unitsubm  20289  dfrhm2  20377  isrhm2d  20390  idrhm  20393  pwsco1rhm  20405  pwsco2rhm  20406  c0rhm  20437  c0rnghm  20438  subrgcrng  20478  subrgsubm  20488  issubrg3  20503  cntzsubr  20509  pwsdiagrhm  20510  isdomn3  20618  subrgacs  20703  cnfldexp  21329  expmhm  21361  nn0srg  21362  rge0srg  21363  fermltlchr  21454  freshmansdream  21499  frobrhm  21500  assamulgscmlem2  21825  psrcrng  21897  mplcoe3  21961  mplcoe5lem  21962  mplcoe5  21963  evlsgsummul  22015  mhppwdeg  22053  psdpw  22073  ply1moncl  22173  coe1pwmul  22181  ply1coefsupp  22200  ply1coe  22201  gsummoncoe1  22211  lply1binomsc  22214  evls1gsummul  22228  evl1expd  22248  evl1gsummul  22263  evl1scvarpw  22266  evl1scvarpwval  22267  evl1gsummon  22268  evls1fpws  22272  rhmply1mon  22292  ringvcl  22303  mat1mhm  22387  scmatmhm  22437  m1detdiag  22500  mdetdiaglem  22501  m2detleiblem2  22531  mat2pmatmhm  22636  pmatcollpwscmatlem1  22692  mply1topmatcllem  22706  mply1topmatcl  22708  pm2mpghm  22719  pm2mpmhm  22723  monmat2matmon  22727  pm2mp  22728  chpscmatgsumbin  22747  chpscmatgsummon  22748  chfacfscmulcl  22760  chfacfscmul0  22761  chfacfpmmulcl  22764  chfacfpmmul0  22765  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  cayhamlem2  22787  cayhamlem4  22791  nrgtrg  24594  deg1pw  26042  idomrootle  26094  plypf1  26133  efsubm  26476  amgm  26917  wilthlem2  26995  wilthlem3  26996  dchrelbas3  27165  lgsqrlem2  27274  lgsqrlem3  27275  lgsqrlem4  27276  cntrcrng  33036  psgnid  33052  cnmsgn0g  33101  altgnsg  33104  isunit3  33191  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnlem3  33194  elrgspnlem4  33195  elrgspn  33196  0ringcring  33202  domnprodn0  33225  rrgsubm  33233  znfermltl  33313  unitprodclb  33336  ringlsmss  33342  rprmdvdspow  33480  1arithidomlem1  33482  1arithidom  33484  1arithufdlem2  33492  1arithufdlem3  33493  1arithufdlem4  33494  zringfrac  33501  ressply1evls1  33510  evl1deg1  33521  evl1deg2  33522  evl1deg3  33523  gsummoncoe1fzo  33539  ply1degltdimlem  33594  ply1degltdim  33595  assarrginv  33608  evls1fldgencl  33641  rtelextdg2lem  33692  2sqr3minply  33746  cos9thpiminplylem6  33753  cos9thpiminply  33754  iistmd  33868  aks6d1c1p2  42082  aks6d1c1p3  42083  aks6d1c1p6  42087  evl1gprodd  42090  aks6d1c2lem3  42099  idomnnzpownz  42105  aks6d1c5lem3  42110  aks6d1c5lem2  42111  deg1pow  42114  aks6d1c6lem1  42143  aks6d1c6lem2  42144  aks5lem2  42160  aks5lem3a  42162  domnexpgn0cl  42496  abvexp  42505  fidomncyc  42508  evlsvvvallem  42534  evlsvvval  42536  evlsexpval  42540  evlselv  42560  mhphf  42570  hbtlem4  43099  mon1psubm  43172  amgm2d  44171  amgm3d  44172  amgm4d  44173  invginvrid  48352  ply1mulgsumlem4  48375  ply1mulgsum  48376  amgmw2d  49790