Theorem ringmgp 20220

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 2736	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2736	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2736	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20218	. 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 3051  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Mndcmnd 18702  Grpcgrp 18909  mulGrpcmgp 20121  Ringcrg 20214

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-ring 20216

This theorem is referenced by:  mgpf  20229  ringcl  20231  iscrng2  20233  ringass  20234  ringideu  20235  ringidcl  20246  ringidmlem  20249  ringsrg  20278  pwspjmhmmgpd  20307  pwsexpg  20308  unitsubm  20366  dfrhm2  20454  isrhm2d  20466  idrhm  20469  pwsco1rhm  20479  pwsco2rhm  20480  c0rhm  20511  c0rnghm  20512  subrgcrng  20552  subrgsubm  20562  issubrg3  20577  cntzsubr  20583  pwsdiagrhm  20584  isdomn3  20692  subrgacs  20777  cnfldexp  21385  expmhm  21416  nn0srg  21417  rge0srg  21418  fermltlchr  21509  freshmansdream  21554  frobrhm  21555  assamulgscmlem2  21880  psrcrng  21950  mplcoe3  22016  mplcoe5lem  22017  mplcoe5  22018  evlsvvvallem  22069  evlsvvval  22071  evlsgsummul  22075  mhppwdeg  22116  psdpw  22136  ply1moncl  22236  coe1pwmul  22244  ply1coefsupp  22262  ply1coe  22263  gsummoncoe1  22273  lply1binomsc  22276  evls1gsummul  22290  evl1expd  22310  evl1gsummul  22325  evl1scvarpw  22328  evl1scvarpwval  22329  evl1gsummon  22330  evls1fpws  22334  rhmply1mon  22354  ringvcl  22365  mat1mhm  22449  scmatmhm  22499  m1detdiag  22562  mdetdiaglem  22563  m2detleiblem2  22593  mat2pmatmhm  22698  pmatcollpwscmatlem1  22754  mply1topmatcllem  22768  mply1topmatcl  22770  pm2mpghm  22781  pm2mpmhm  22785  monmat2matmon  22789  pm2mp  22790  chpscmatgsumbin  22809  chpscmatgsummon  22810  chfacfscmulcl  22822  chfacfscmul0  22823  chfacfpmmulcl  22826  chfacfpmmul0  22827  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cayhamlem2  22849  cayhamlem4  22853  nrgtrg  24655  deg1pw  26086  idomrootle  26138  plypf1  26177  efsubm  26515  amgm  26954  wilthlem2  27032  wilthlem3  27033  dchrelbas3  27201  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  cntrcrng  33142  psgnid  33158  cnmsgn0g  33207  altgnsg  33210  ringm1expp1  33295  isunit3  33302  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  0ringcring  33313  domnprodn0  33336  rrgsubm  33345  znfermltl  33426  unitprodclb  33449  ringlsmss  33455  rprmdvdspow  33593  1arithidomlem1  33595  1arithidom  33597  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  zringfrac  33614  ressply1evls1  33625  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  evls1monply1  33639  ply1coedeg  33649  gsummoncoe1fzo  33657  vietalem  33723  ply1degltdimlem  33766  ply1degltdim  33767  assarrginv  33780  evls1fldgencl  33814  extdgfialglem1  33836  extdgfialglem2  33837  rtelextdg2lem  33870  2sqr3minply  33924  cos9thpiminplylem6  33931  cos9thpiminply  33932  iistmd  34046  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p6  42553  evl1gprodd  42556  aks6d1c2lem3  42565  idomnnzpownz  42571  aks6d1c5lem3  42576  aks6d1c5lem2  42577  deg1pow  42580  aks6d1c6lem1  42609  aks6d1c6lem2  42610  aks5lem2  42626  aks5lem3a  42628  domnexpgn0cl  42968  abvexp  42977  fidomncyc  42980  evlsexpval  43003  evlselv  43020  mhphf  43030  hbtlem4  43554  mon1psubm  43627  amgm2d  44625  amgm3d  44626  amgm4d  44627  invginvrid  48843  ply1mulgsumlem4  48865  ply1mulgsum  48866  amgmw2d  50279