Theorem ringmgp 20167

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 2733	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2733	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2733	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20165	. 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 1541   ∈ wcel 2113  ∀wral 3049  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  +_gcplusg 17171  ._rcmulr 17172  Mndcmnd 18652  Grpcgrp 18856  mulGrpcmgp 20068  Ringcrg 20161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-ring 20163

This theorem is referenced by:  mgpf  20176  ringcl  20178  iscrng2  20180  ringass  20181  ringideu  20182  ringidcl  20193  ringidmlem  20196  ringsrg  20225  pwspjmhmmgpd  20256  pwsexpg  20257  unitsubm  20314  dfrhm2  20402  isrhm2d  20414  idrhm  20417  pwsco1rhm  20427  pwsco2rhm  20428  c0rhm  20459  c0rnghm  20460  subrgcrng  20500  subrgsubm  20510  issubrg3  20525  cntzsubr  20531  pwsdiagrhm  20532  isdomn3  20640  subrgacs  20725  cnfldexp  21351  expmhm  21383  nn0srg  21384  rge0srg  21385  fermltlchr  21476  freshmansdream  21521  frobrhm  21522  assamulgscmlem2  21847  psrcrng  21919  mplcoe3  21983  mplcoe5lem  21984  mplcoe5  21985  evlsgsummul  22037  mhppwdeg  22075  psdpw  22095  ply1moncl  22195  coe1pwmul  22203  ply1coefsupp  22222  ply1coe  22223  gsummoncoe1  22233  lply1binomsc  22236  evls1gsummul  22250  evl1expd  22270  evl1gsummul  22285  evl1scvarpw  22288  evl1scvarpwval  22289  evl1gsummon  22290  evls1fpws  22294  rhmply1mon  22314  ringvcl  22325  mat1mhm  22409  scmatmhm  22459  m1detdiag  22522  mdetdiaglem  22523  m2detleiblem2  22553  mat2pmatmhm  22658  pmatcollpwscmatlem1  22714  mply1topmatcllem  22728  mply1topmatcl  22730  pm2mpghm  22741  pm2mpmhm  22745  monmat2matmon  22749  pm2mp  22750  chpscmatgsumbin  22769  chpscmatgsummon  22770  chfacfscmulcl  22782  chfacfscmul0  22783  chfacfpmmulcl  22786  chfacfpmmul0  22787  chfacfpmmulgsum2  22790  cayhamlem1  22791  cpmadugsumlemB  22799  cpmadugsumlemC  22800  cpmadugsumlemF  22801  cayhamlem2  22809  cayhamlem4  22813  nrgtrg  24615  deg1pw  26063  idomrootle  26115  plypf1  26154  efsubm  26497  amgm  26938  wilthlem2  27016  wilthlem3  27017  dchrelbas3  27186  lgsqrlem2  27295  lgsqrlem3  27296  lgsqrlem4  27297  cntrcrng  33061  psgnid  33077  cnmsgn0g  33126  altgnsg  33129  isunit3  33219  elrgspnlem1  33220  elrgspnlem2  33221  elrgspnlem3  33222  elrgspnlem4  33223  elrgspn  33224  0ringcring  33230  domnprodn0  33253  rrgsubm  33261  znfermltl  33342  unitprodclb  33365  ringlsmss  33371  rprmdvdspow  33509  1arithidomlem1  33511  1arithidom  33513  1arithufdlem2  33521  1arithufdlem3  33522  1arithufdlem4  33523  zringfrac  33530  ressply1evls1  33539  evl1deg1  33550  evl1deg2  33551  evl1deg3  33552  evls1monply1  33553  gsummoncoe1fzo  33569  ply1degltdimlem  33646  ply1degltdim  33647  assarrginv  33660  evls1fldgencl  33694  extdgfialglem1  33716  extdgfialglem2  33717  rtelextdg2lem  33750  2sqr3minply  33804  cos9thpiminplylem6  33811  cos9thpiminply  33812  iistmd  33926  aks6d1c1p2  42212  aks6d1c1p3  42213  aks6d1c1p6  42217  evl1gprodd  42220  aks6d1c2lem3  42229  idomnnzpownz  42235  aks6d1c5lem3  42240  aks6d1c5lem2  42241  deg1pow  42244  aks6d1c6lem1  42273  aks6d1c6lem2  42274  aks5lem2  42290  aks5lem3a  42292  domnexpgn0cl  42631  abvexp  42640  fidomncyc  42643  evlsvvvallem  42669  evlsvvval  42671  evlsexpval  42675  evlselv  42695  mhphf  42705  hbtlem4  43233  mon1psubm  43306  amgm2d  44305  amgm3d  44306  amgm4d  44307  invginvrid  48481  ply1mulgsumlem4  48504  ply1mulgsum  48505  amgmw2d  49919