Theorem ringmgp 20155

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 2731	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2731	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2731	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20153	. 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 2111  ∀wral 3047  ‘cfv 6481  (class class class)co 7346  Basecbs 17117  +_gcplusg 17158  ._rcmulr 17159  Mndcmnd 18639  Grpcgrp 18843  mulGrpcmgp 20056  Ringcrg 20149

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-ring 20151

This theorem is referenced by:  mgpf  20164  ringcl  20166  iscrng2  20168  ringass  20169  ringideu  20170  ringidcl  20181  ringidmlem  20184  ringsrg  20213  pwspjmhmmgpd  20244  pwsexpg  20245  unitsubm  20302  dfrhm2  20390  isrhm2d  20402  idrhm  20405  pwsco1rhm  20415  pwsco2rhm  20416  c0rhm  20447  c0rnghm  20448  subrgcrng  20488  subrgsubm  20498  issubrg3  20513  cntzsubr  20519  pwsdiagrhm  20520  isdomn3  20628  subrgacs  20713  cnfldexp  21339  expmhm  21371  nn0srg  21372  rge0srg  21373  fermltlchr  21464  freshmansdream  21509  frobrhm  21510  assamulgscmlem2  21835  psrcrng  21907  mplcoe3  21971  mplcoe5lem  21972  mplcoe5  21973  evlsgsummul  22025  mhppwdeg  22063  psdpw  22083  ply1moncl  22183  coe1pwmul  22191  ply1coefsupp  22210  ply1coe  22211  gsummoncoe1  22221  lply1binomsc  22224  evls1gsummul  22238  evl1expd  22258  evl1gsummul  22273  evl1scvarpw  22276  evl1scvarpwval  22277  evl1gsummon  22278  evls1fpws  22282  rhmply1mon  22302  ringvcl  22313  mat1mhm  22397  scmatmhm  22447  m1detdiag  22510  mdetdiaglem  22511  m2detleiblem2  22541  mat2pmatmhm  22646  pmatcollpwscmatlem1  22702  mply1topmatcllem  22716  mply1topmatcl  22718  pm2mpghm  22729  pm2mpmhm  22733  monmat2matmon  22737  pm2mp  22738  chpscmatgsumbin  22757  chpscmatgsummon  22758  chfacfscmulcl  22770  chfacfscmul0  22771  chfacfpmmulcl  22774  chfacfpmmul0  22775  chfacfpmmulgsum2  22778  cayhamlem1  22779  cpmadugsumlemB  22787  cpmadugsumlemC  22788  cpmadugsumlemF  22789  cayhamlem2  22797  cayhamlem4  22801  nrgtrg  24603  deg1pw  26051  idomrootle  26103  plypf1  26142  efsubm  26485  amgm  26926  wilthlem2  27004  wilthlem3  27005  dchrelbas3  27174  lgsqrlem2  27283  lgsqrlem3  27284  lgsqrlem4  27285  cntrcrng  33045  psgnid  33061  cnmsgn0g  33110  altgnsg  33113  isunit3  33203  elrgspnlem1  33204  elrgspnlem2  33205  elrgspnlem3  33206  elrgspnlem4  33207  elrgspn  33208  0ringcring  33214  domnprodn0  33237  rrgsubm  33245  znfermltl  33326  unitprodclb  33349  ringlsmss  33355  rprmdvdspow  33493  1arithidomlem1  33495  1arithidom  33497  1arithufdlem2  33505  1arithufdlem3  33506  1arithufdlem4  33507  zringfrac  33514  ressply1evls1  33523  evl1deg1  33534  evl1deg2  33535  evl1deg3  33536  evls1monply1  33537  gsummoncoe1fzo  33553  ply1degltdimlem  33630  ply1degltdim  33631  assarrginv  33644  evls1fldgencl  33678  extdgfialglem1  33700  extdgfialglem2  33701  rtelextdg2lem  33734  2sqr3minply  33788  cos9thpiminplylem6  33795  cos9thpiminply  33796  iistmd  33910  aks6d1c1p2  42141  aks6d1c1p3  42142  aks6d1c1p6  42146  evl1gprodd  42149  aks6d1c2lem3  42158  idomnnzpownz  42164  aks6d1c5lem3  42169  aks6d1c5lem2  42170  deg1pow  42173  aks6d1c6lem1  42202  aks6d1c6lem2  42203  aks5lem2  42219  aks5lem3a  42221  domnexpgn0cl  42555  abvexp  42564  fidomncyc  42567  evlsvvvallem  42593  evlsvvval  42595  evlsexpval  42599  evlselv  42619  mhphf  42629  hbtlem4  43158  mon1psubm  43231  amgm2d  44230  amgm3d  44231  amgm4d  44232  invginvrid  48397  ply1mulgsumlem4  48420  ply1mulgsum  48421  amgmw2d  49835