Theorem ringmgp 20384

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  +_gcplusg 17348  ._rcmulr 17349  Mndcmnd 18842  Grpcgrp 19063  mulGrpcmgp 20279  Ringcrg 20378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-ring 20380

This theorem is used by:  mgpf  20393  ringcl  20395  iscrng2  20397  ringass  20398  ringideu  20399  ringidcl  20412  ringidmlem  20415  dfring2  20435  ringsrg  20445  pwspjmhmmgpd  20474  pwsexpg  20475  unitsubm  20533  dfrhm2  20621  isrhm2d  20638  idrhm  20642  pwsco1rhm  20658  pwsco2rhm  20659  c0rhm  20702  c0rnghm  20703  subrgcrng  20743  subrgsubm  20753  issubrg3  20768  cntzsubr  20774  pwsdiagrhm  20775  isdomn3  20882  isdrng3lem1  20920  subrgacs  20972  prmidlsubm  21556  cnfldexp  21624  expmhm  21655  nn0srg  21656  rge0srg  21657  fermltlchr  21748  freshmansdream  21793  frobrhm  21794  assamulgscmlem2  22121  psrcrng  22192  mplcoe3  22260  mplcoe5lem  22261  mplcoe5  22262  evlsvvvallem  22313  evlsvvval  22315  evlsgsummul  22319  evlsexpval  22350  mhppwdeg  22384  psdpw  22404  ply1moncl  22503  coe1pwmul  22511  ply1coefsupp  22528  ply1coe  22529  gsummoncoe1  22539  lply1binomsc  22542  evls1gsummul  22556  evl1expd  22576  evl1gsummul  22591  evl1scvarpw  22594  evl1scvarpwval  22595  evl1gsummon  22596  evls1fpws  22600  rhmply1mon  22617  ringvcl  22628  mat1mhm  22712  scmatmhm  22762  m1detdiag  22825  mdetdiaglem  22826  m2detleiblem2  22856  mat2pmatmhm  22964  pmatcollpwscmatlem1  23020  mply1topmatcllem  23034  mply1topmatcl  23036  pm2mpghm  23047  pm2mpmhm  23051  monmat2matmon  23055  pm2mp  23056  chpscmatgsumbin  23075  chpscmatgsummon  23076  chfacfscmulcl  23088  chfacfscmul0  23089  chfacfpmmulcl  23092  chfacfpmmul0  23093  chfacfpmmulgsum2  23096  cayhamlem1  23097  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  cayhamlem2  23115  cayhamlem4  23119  nrgtrg  24922  deg1pw  26353  idomrootle  26405  plypf1  26445  efsubm  26796  amgm  27235  wilthlem2  27313  wilthlem3  27314  dchrelbas3  27482  lgsqrlem2  27591  lgsqrlem3  27592  lgsqrlem4  27593  cntrcrng  33529  psgnid  33545  cnmsgn0g  33594  altgnsg  33597  ringm1expp1  33681  isunit3  33688  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem3  33692  elrgspnlem4  33693  elrgspn  33694  0ringcring  33700  domnprodn0  33726  rrgsubm  33732  znfermltl  33809  unitprodclb  33830  ringlsmss  33834  rprmdvdspow  33951  1arithidomlem1  33953  1arithidom  33955  1arithufdlem2  33963  1arithufdlem3  33964  1arithufdlem4  33965  zringfrac  33972  ressply1evls1  33983  evl1deg1  33994  evl1deg2  33995  evl1deg3  33996  evls1monply1  33997  ply1coedeg  34007  gsummoncoe1fzo  34015  vietalem  34097  ply1degltdimlem  34140  ply1degltdim  34141  assarrginv  34154  evls1fldgencl  34188  extdgfialglem1  34210  extdgfialglem2  34211  rtelextdg2lem  34244  2sqr3minply  34298  cos9thpiminplylem6  34305  cos9thpiminply  34306  iistmd  34420  aks6d1c1p2  42983  aks6d1c1p3  42984  aks6d1c1p6  42988  evl1gprodd  42991  aks6d1c2lem3  43000  idomnnzpownz  43006  aks6d1c5lem3  43011  aks6d1c5lem2  43012  deg1pow  43015  aks6d1c6lem1  43044  aks6d1c6lem2  43045  aks5lem2  43061  aks5lem3a  43063  domnexpgn0cl  43413  abvexp  43422  fidomncyc  43425  evlselv  43443  mhphf  43451  hbtlem4  43975  mon1psubm  44048  amgm2d  45046  amgm3d  45047  amgm4d  45048  invginvrid  49305  ply1mulgsumlem4  49327  ply1mulgsum  49328  amgmw2d  50830