Theorem ringmgp 20211

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 20209	. 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 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212  Mndcmnd 18693  Grpcgrp 18900  mulGrpcmgp 20112  Ringcrg 20205

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 5241

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-ring 20207

This theorem is referenced by:  mgpf  20220  ringcl  20222  iscrng2  20224  ringass  20225  ringideu  20226  ringidcl  20237  ringidmlem  20240  ringsrg  20269  pwspjmhmmgpd  20298  pwsexpg  20299  unitsubm  20357  dfrhm2  20445  isrhm2d  20457  idrhm  20460  pwsco1rhm  20470  pwsco2rhm  20471  c0rhm  20502  c0rnghm  20503  subrgcrng  20543  subrgsubm  20553  issubrg3  20568  cntzsubr  20574  pwsdiagrhm  20575  isdomn3  20683  subrgacs  20768  cnfldexp  21394  expmhm  21426  nn0srg  21427  rge0srg  21428  fermltlchr  21519  freshmansdream  21564  frobrhm  21565  assamulgscmlem2  21890  psrcrng  21960  mplcoe3  22026  mplcoe5lem  22027  mplcoe5  22028  evlsvvvallem  22079  evlsvvval  22081  evlsgsummul  22085  mhppwdeg  22126  psdpw  22146  ply1moncl  22246  coe1pwmul  22254  ply1coefsupp  22272  ply1coe  22273  gsummoncoe1  22283  lply1binomsc  22286  evls1gsummul  22300  evl1expd  22320  evl1gsummul  22335  evl1scvarpw  22338  evl1scvarpwval  22339  evl1gsummon  22340  evls1fpws  22344  rhmply1mon  22364  ringvcl  22375  mat1mhm  22459  scmatmhm  22509  m1detdiag  22572  mdetdiaglem  22573  m2detleiblem2  22603  mat2pmatmhm  22708  pmatcollpwscmatlem1  22764  mply1topmatcllem  22778  mply1topmatcl  22780  pm2mpghm  22791  pm2mpmhm  22795  monmat2matmon  22799  pm2mp  22800  chpscmatgsumbin  22819  chpscmatgsummon  22820  chfacfscmulcl  22832  chfacfscmul0  22833  chfacfpmmulcl  22836  chfacfpmmul0  22837  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  cayhamlem2  22859  cayhamlem4  22863  nrgtrg  24665  deg1pw  26096  idomrootle  26148  plypf1  26187  efsubm  26528  amgm  26968  wilthlem2  27046  wilthlem3  27047  dchrelbas3  27215  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  cntrcrng  33157  psgnid  33173  cnmsgn0g  33222  altgnsg  33225  ringm1expp1  33310  isunit3  33317  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspn  33322  0ringcring  33328  domnprodn0  33351  rrgsubm  33360  znfermltl  33441  unitprodclb  33464  ringlsmss  33470  rprmdvdspow  33608  1arithidomlem1  33610  1arithidom  33612  1arithufdlem2  33620  1arithufdlem3  33621  1arithufdlem4  33622  zringfrac  33629  ressply1evls1  33640  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  evls1monply1  33654  ply1coedeg  33664  gsummoncoe1fzo  33672  vietalem  33738  ply1degltdimlem  33782  ply1degltdim  33783  assarrginv  33796  evls1fldgencl  33830  extdgfialglem1  33852  extdgfialglem2  33853  rtelextdg2lem  33886  2sqr3minply  33940  cos9thpiminplylem6  33947  cos9thpiminply  33948  iistmd  34062  aks6d1c1p2  42562  aks6d1c1p3  42563  aks6d1c1p6  42567  evl1gprodd  42570  aks6d1c2lem3  42579  idomnnzpownz  42585  aks6d1c5lem3  42590  aks6d1c5lem2  42591  deg1pow  42594  aks6d1c6lem1  42623  aks6d1c6lem2  42624  aks5lem2  42640  aks5lem3a  42642  domnexpgn0cl  42982  abvexp  42991  fidomncyc  42994  evlsexpval  43017  evlselv  43034  mhphf  43044  hbtlem4  43572  mon1psubm  43645  amgm2d  44643  amgm3d  44644  amgm4d  44645  invginvrid  48855  ply1mulgsumlem4  48877  ply1mulgsum  48878  amgmw2d  50291