Theorem ringmgp 20322

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  ._rcmulr 17312  Mndcmnd 18793  Grpcgrp 19001  mulGrpcmgp 20217  Ringcrg 20316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-ring 20318

This theorem is referenced by:  mgpf  20331  ringcl  20333  iscrng2  20335  ringass  20336  ringideu  20337  ringidcl  20349  ringidmlem  20352  ringsrg  20381  pwspjmhmmgpd  20410  pwsexpg  20411  unitsubm  20469  dfrhm2  20557  isrhm2d  20570  idrhm  20573  pwsco1rhm  20585  pwsco2rhm  20586  c0rhm  20620  c0rnghm  20621  subrgcrng  20661  subrgsubm  20671  issubrg3  20686  cntzsubr  20692  pwsdiagrhm  20693  isdomn3  20800  subrgacs  20884  prmidlsubm  21468  cnfldexp  21536  expmhm  21567  nn0srg  21568  rge0srg  21569  fermltlchr  21660  freshmansdream  21705  frobrhm  21706  assamulgscmlem2  22031  psrcrng  22102  mplcoe3  22170  mplcoe5lem  22171  mplcoe5  22172  evlsvvvallem  22223  evlsvvval  22225  evlsgsummul  22229  evlsexpval  22260  mhppwdeg  22294  psdpw  22314  ply1moncl  22413  coe1pwmul  22421  ply1coefsupp  22438  ply1coe  22439  gsummoncoe1  22449  lply1binomsc  22452  evls1gsummul  22466  evl1expd  22486  evl1gsummul  22501  evl1scvarpw  22504  evl1scvarpwval  22505  evl1gsummon  22506  evls1fpws  22510  rhmply1mon  22527  ringvcl  22538  mat1mhm  22622  scmatmhm  22672  m1detdiag  22735  mdetdiaglem  22736  m2detleiblem2  22766  mat2pmatmhm  22871  pmatcollpwscmatlem1  22927  mply1topmatcllem  22941  mply1topmatcl  22943  pm2mpghm  22954  pm2mpmhm  22958  monmat2matmon  22962  pm2mp  22963  chpscmatgsumbin  22982  chpscmatgsummon  22983  chfacfscmulcl  22995  chfacfscmul0  22996  chfacfpmmulcl  22999  chfacfpmmul0  23000  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  cayhamlem2  23022  cayhamlem4  23026  nrgtrg  24828  deg1pw  26259  idomrootle  26311  plypf1  26350  efsubm  26694  amgm  27133  wilthlem2  27211  wilthlem3  27212  dchrelbas3  27380  lgsqrlem2  27489  lgsqrlem3  27490  lgsqrlem4  27491  cntrcrng  33379  psgnid  33395  cnmsgn0g  33444  altgnsg  33447  ringm1expp1  33531  isunit3  33538  elrgspnlem1  33540  elrgspnlem2  33541  elrgspnlem3  33542  elrgspnlem4  33543  elrgspn  33544  0ringcring  33550  domnprodn0  33576  rrgsubm  33582  znfermltl  33659  unitprodclb  33680  ringlsmss  33684  rprmdvdspow  33801  1arithidomlem1  33803  1arithidom  33805  1arithufdlem2  33813  1arithufdlem3  33814  1arithufdlem4  33815  zringfrac  33822  ressply1evls1  33833  evl1deg1  33844  evl1deg2  33845  evl1deg3  33846  evls1monply1  33847  ply1coedeg  33857  gsummoncoe1fzo  33865  vietalem  33947  ply1degltdimlem  33990  ply1degltdim  33991  assarrginv  34004  evls1fldgencl  34038  extdgfialglem1  34060  extdgfialglem2  34061  rtelextdg2lem  34094  2sqr3minply  34148  cos9thpiminplylem6  34155  cos9thpiminply  34156  iistmd  34270  aks6d1c1p2  42854  aks6d1c1p3  42855  aks6d1c1p6  42859  evl1gprodd  42862  aks6d1c2lem3  42871  idomnnzpownz  42877  aks6d1c5lem3  42882  aks6d1c5lem2  42883  deg1pow  42886  aks6d1c6lem1  42915  aks6d1c6lem2  42916  aks5lem2  42932  aks5lem3a  42934  domnexpgn0cl  43271  abvexp  43280  fidomncyc  43283  evlselv  43301  mhphf  43309  hbtlem4  43833  mon1psubm  43906  amgm2d  44904  amgm3d  44905  amgm4d  44906  invginvrid  49124  ply1mulgsumlem4  49146  ply1mulgsum  49147  amgmw2d  50581