Theorem ringmgp 20352

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 2766	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2766	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2766	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20350	. 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 2146  ∀wral 3082  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  ._rcmulr 17336  Mndcmnd 18821  Grpcgrp 19031  mulGrpcmgp 20247  Ringcrg 20346

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-ring 20348

This theorem is used by:  mgpf  20361  ringcl  20363  iscrng2  20365  ringass  20366  ringideu  20367  ringidcl  20380  ringidmlem  20383  dfring2  20403  ringsrg  20413  pwspjmhmmgpd  20442  pwsexpg  20443  unitsubm  20501  dfrhm2  20589  isrhm2d  20606  idrhm  20610  pwsco1rhm  20626  pwsco2rhm  20627  c0rhm  20670  c0rnghm  20671  subrgcrng  20711  subrgsubm  20721  issubrg3  20736  cntzsubr  20742  pwsdiagrhm  20743  isdomn3  20850  isdrng3lem1  20888  subrgacs  20940  prmidlsubm  21524  cnfldexp  21592  expmhm  21623  nn0srg  21624  rge0srg  21625  fermltlchr  21716  freshmansdream  21761  frobrhm  21762  assamulgscmlem2  22087  psrcrng  22158  mplcoe3  22226  mplcoe5lem  22227  mplcoe5  22228  evlsvvvallem  22279  evlsvvval  22281  evlsgsummul  22285  evlsexpval  22316  mhppwdeg  22350  psdpw  22370  ply1moncl  22469  coe1pwmul  22477  ply1coefsupp  22494  ply1coe  22495  gsummoncoe1  22505  lply1binomsc  22508  evls1gsummul  22522  evl1expd  22542  evl1gsummul  22557  evl1scvarpw  22560  evl1scvarpwval  22561  evl1gsummon  22562  evls1fpws  22566  rhmply1mon  22583  ringvcl  22594  mat1mhm  22678  scmatmhm  22728  m1detdiag  22791  mdetdiaglem  22792  m2detleiblem2  22822  mat2pmatmhm  22927  pmatcollpwscmatlem1  22983  mply1topmatcllem  22997  mply1topmatcl  22999  pm2mpghm  23010  pm2mpmhm  23014  monmat2matmon  23018  pm2mp  23019  chpscmatgsumbin  23038  chpscmatgsummon  23039  chfacfscmulcl  23051  chfacfscmul0  23052  chfacfpmmulcl  23055  chfacfpmmul0  23056  chfacfpmmulgsum2  23059  cayhamlem1  23060  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  cayhamlem2  23078  cayhamlem4  23082  nrgtrg  24884  deg1pw  26315  idomrootle  26367  plypf1  26406  efsubm  26753  amgm  27192  wilthlem2  27270  wilthlem3  27271  dchrelbas3  27439  lgsqrlem2  27548  lgsqrlem3  27549  lgsqrlem4  27550  cntrcrng  33432  psgnid  33448  cnmsgn0g  33497  altgnsg  33500  ringm1expp1  33584  isunit3  33591  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem3  33595  elrgspnlem4  33596  elrgspn  33597  0ringcring  33603  domnprodn0  33629  rrgsubm  33635  znfermltl  33712  unitprodclb  33733  ringlsmss  33737  rprmdvdspow  33854  1arithidomlem1  33856  1arithidom  33858  1arithufdlem2  33866  1arithufdlem3  33867  1arithufdlem4  33868  zringfrac  33875  ressply1evls1  33886  evl1deg1  33897  evl1deg2  33898  evl1deg3  33899  evls1monply1  33900  ply1coedeg  33910  gsummoncoe1fzo  33918  vietalem  34000  ply1degltdimlem  34043  ply1degltdim  34044  assarrginv  34057  evls1fldgencl  34091  extdgfialglem1  34113  extdgfialglem2  34114  rtelextdg2lem  34147  2sqr3minply  34201  cos9thpiminplylem6  34208  cos9thpiminply  34209  iistmd  34323  aks6d1c1p2  42916  aks6d1c1p3  42917  aks6d1c1p6  42921  evl1gprodd  42924  aks6d1c2lem3  42933  idomnnzpownz  42939  aks6d1c5lem3  42944  aks6d1c5lem2  42945  deg1pow  42948  aks6d1c6lem1  42977  aks6d1c6lem2  42978  aks5lem2  42994  aks5lem3a  42996  domnexpgn0cl  43331  abvexp  43340  fidomncyc  43343  evlselv  43361  mhphf  43369  hbtlem4  43893  mon1psubm  43966  amgm2d  44964  amgm3d  44965  amgm4d  44966  invginvrid  49187  ply1mulgsumlem4  49209  ply1mulgsum  49210  amgmw2d  50692