Theorem ringmgp 20174

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 20172	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp2bi 1146	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  ._rcmulr 17178  Mndcmnd 18659  Grpcgrp 18863  mulGrpcmgp 20075  Ringcrg 20168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-ring 20170

This theorem is referenced by:  mgpf  20183  ringcl  20185  iscrng2  20187  ringass  20188  ringideu  20189  ringidcl  20200  ringidmlem  20203  ringsrg  20232  pwspjmhmmgpd  20263  pwsexpg  20264  unitsubm  20322  dfrhm2  20410  isrhm2d  20422  idrhm  20425  pwsco1rhm  20435  pwsco2rhm  20436  c0rhm  20467  c0rnghm  20468  subrgcrng  20508  subrgsubm  20518  issubrg3  20533  cntzsubr  20539  pwsdiagrhm  20540  isdomn3  20648  subrgacs  20733  cnfldexp  21359  expmhm  21391  nn0srg  21392  rge0srg  21393  fermltlchr  21484  freshmansdream  21529  frobrhm  21530  assamulgscmlem2  21856  psrcrng  21927  mplcoe3  21993  mplcoe5lem  21994  mplcoe5  21995  evlsvvvallem  22046  evlsvvval  22048  evlsgsummul  22052  mhppwdeg  22093  psdpw  22113  ply1moncl  22213  coe1pwmul  22221  ply1coefsupp  22241  ply1coe  22242  gsummoncoe1  22252  lply1binomsc  22255  evls1gsummul  22269  evl1expd  22289  evl1gsummul  22304  evl1scvarpw  22307  evl1scvarpwval  22308  evl1gsummon  22309  evls1fpws  22313  rhmply1mon  22333  ringvcl  22344  mat1mhm  22428  scmatmhm  22478  m1detdiag  22541  mdetdiaglem  22542  m2detleiblem2  22572  mat2pmatmhm  22677  pmatcollpwscmatlem1  22733  mply1topmatcllem  22747  mply1topmatcl  22749  pm2mpghm  22760  pm2mpmhm  22764  monmat2matmon  22768  pm2mp  22769  chpscmatgsumbin  22788  chpscmatgsummon  22789  chfacfscmulcl  22801  chfacfscmul0  22802  chfacfpmmulcl  22805  chfacfpmmul0  22806  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cayhamlem2  22828  cayhamlem4  22832  nrgtrg  24634  deg1pw  26082  idomrootle  26134  plypf1  26173  efsubm  26516  amgm  26957  wilthlem2  27035  wilthlem3  27036  dchrelbas3  27205  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  cntrcrng  33163  psgnid  33179  cnmsgn0g  33228  altgnsg  33231  ringm1expp1  33316  isunit3  33323  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspn  33328  0ringcring  33334  domnprodn0  33357  rrgsubm  33366  znfermltl  33447  unitprodclb  33470  ringlsmss  33476  rprmdvdspow  33614  1arithidomlem1  33616  1arithidom  33618  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  zringfrac  33635  ressply1evls1  33646  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  evls1monply1  33660  ply1coedeg  33670  gsummoncoe1fzo  33678  vietalem  33735  ply1degltdimlem  33779  ply1degltdim  33780  assarrginv  33793  evls1fldgencl  33827  extdgfialglem1  33849  extdgfialglem2  33850  rtelextdg2lem  33883  2sqr3minply  33937  cos9thpiminplylem6  33944  cos9thpiminply  33945  iistmd  34059  aks6d1c1p2  42359  aks6d1c1p3  42360  aks6d1c1p6  42364  evl1gprodd  42367  aks6d1c2lem3  42376  idomnnzpownz  42382  aks6d1c5lem3  42387  aks6d1c5lem2  42388  deg1pow  42391  aks6d1c6lem1  42420  aks6d1c6lem2  42421  aks5lem2  42437  aks5lem3a  42439  domnexpgn0cl  42774  abvexp  42783  fidomncyc  42786  evlsexpval  42809  evlselv  42826  mhphf  42836  hbtlem4  43364  mon1psubm  43437  amgm2d  44435  amgm3d  44436  amgm4d  44437  invginvrid  48609  ply1mulgsumlem4  48631  ply1mulgsum  48632  amgmw2d  50045