Theorem ringmgp 20312

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ‘cfv 6525  (class class class)co 7400  Basecbs 17259  +_gcplusg 17300  ._rcmulr 17301  Mndcmnd 18782  Grpcgrp 18990  mulGrpcmgp 20207  Ringcrg 20306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-ring 20308

This theorem is referenced by:  mgpf  20321  ringcl  20323  iscrng2  20325  ringass  20326  ringideu  20327  ringidcl  20339  ringidmlem  20342  ringsrg  20371  pwspjmhmmgpd  20400  pwsexpg  20401  unitsubm  20459  dfrhm2  20547  isrhm2d  20560  idrhm  20563  pwsco1rhm  20575  pwsco2rhm  20576  c0rhm  20610  c0rnghm  20611  subrgcrng  20651  subrgsubm  20661  issubrg3  20676  cntzsubr  20682  pwsdiagrhm  20683  isdomn3  20790  subrgacs  20872  prmidlsubm  21447  cnfldexp  21515  expmhm  21546  nn0srg  21547  rge0srg  21548  fermltlchr  21639  freshmansdream  21684  frobrhm  21685  assamulgscmlem2  22010  psrcrng  22081  mplcoe3  22149  mplcoe5lem  22150  mplcoe5  22151  evlsvvvallem  22202  evlsvvval  22204  evlsgsummul  22208  evlsexpval  22239  mhppwdeg  22273  psdpw  22293  ply1moncl  22392  coe1pwmul  22400  ply1coefsupp  22418  ply1coe  22419  gsummoncoe1  22429  lply1binomsc  22432  evls1gsummul  22446  evl1expd  22466  evl1gsummul  22481  evl1scvarpw  22484  evl1scvarpwval  22485  evl1gsummon  22486  evls1fpws  22490  rhmply1mon  22507  ringvcl  22518  mat1mhm  22602  scmatmhm  22652  m1detdiag  22715  mdetdiaglem  22716  m2detleiblem2  22746  mat2pmatmhm  22851  pmatcollpwscmatlem1  22907  mply1topmatcllem  22921  mply1topmatcl  22923  pm2mpghm  22934  pm2mpmhm  22938  monmat2matmon  22942  pm2mp  22943  chpscmatgsumbin  22962  chpscmatgsummon  22963  chfacfscmulcl  22975  chfacfscmul0  22976  chfacfpmmulcl  22979  chfacfpmmul0  22980  chfacfpmmulgsum2  22983  cayhamlem1  22984  cpmadugsumlemB  22992  cpmadugsumlemC  22993  cpmadugsumlemF  22994  cayhamlem2  23002  cayhamlem4  23006  nrgtrg  24808  deg1pw  26239  idomrootle  26291  plypf1  26330  efsubm  26674  amgm  27113  wilthlem2  27191  wilthlem3  27192  dchrelbas3  27360  lgsqrlem2  27469  lgsqrlem3  27470  lgsqrlem4  27471  cntrcrng  33314  psgnid  33330  cnmsgn0g  33379  altgnsg  33382  ringm1expp1  33466  isunit3  33473  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnlem3  33477  elrgspnlem4  33478  elrgspn  33479  0ringcring  33485  domnprodn0  33511  rrgsubm  33517  znfermltl  33596  unitprodclb  33618  ringlsmss  33622  rprmdvdspow  33740  1arithidomlem1  33742  1arithidom  33744  1arithufdlem2  33752  1arithufdlem3  33753  1arithufdlem4  33754  zringfrac  33761  ressply1evls1  33772  evl1deg1  33783  evl1deg2  33784  evl1deg3  33785  evls1monply1  33786  ply1coedeg  33796  gsummoncoe1fzo  33804  vietalem  33886  ply1degltdimlem  33929  ply1degltdim  33930  assarrginv  33943  evls1fldgencl  33977  extdgfialglem1  33999  extdgfialglem2  34000  rtelextdg2lem  34033  2sqr3minply  34087  cos9thpiminplylem6  34094  cos9thpiminply  34095  iistmd  34209  aks6d1c1p2  42738  aks6d1c1p3  42739  aks6d1c1p6  42743  evl1gprodd  42746  aks6d1c2lem3  42755  idomnnzpownz  42761  aks6d1c5lem3  42766  aks6d1c5lem2  42767  deg1pow  42770  aks6d1c6lem1  42799  aks6d1c6lem2  42800  aks5lem2  42816  aks5lem3a  42818  domnexpgn0cl  43153  abvexp  43162  fidomncyc  43165  evlselv  43183  mhphf  43191  hbtlem4  43715  mon1psubm  43788  amgm2d  44786  amgm3d  44787  amgm4d  44788  invginvrid  48998  ply1mulgsumlem4  49020  ply1mulgsum  49021  amgmw2d  50433