Theorem ringmgp 20148

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 2729	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2729	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2729	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20146	. 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 1540   ∈ wcel 2109  ∀wral 3044  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Mndcmnd 18661  Grpcgrp 18865  mulGrpcmgp 20049  Ringcrg 20142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-ring 20144

This theorem is referenced by:  mgpf  20157  ringcl  20159  iscrng2  20161  ringass  20162  ringideu  20163  ringidcl  20174  ringidmlem  20177  ringsrg  20206  pwspjmhmmgpd  20237  pwsexpg  20238  unitsubm  20295  dfrhm2  20383  isrhm2d  20396  idrhm  20399  pwsco1rhm  20411  pwsco2rhm  20412  c0rhm  20443  c0rnghm  20444  subrgcrng  20484  subrgsubm  20494  issubrg3  20509  cntzsubr  20515  pwsdiagrhm  20516  isdomn3  20624  subrgacs  20709  cnfldexp  21316  expmhm  21353  nn0srg  21354  rge0srg  21355  fermltlchr  21439  freshmansdream  21484  frobrhm  21485  assamulgscmlem2  21809  psrcrng  21881  mplcoe3  21945  mplcoe5lem  21946  mplcoe5  21947  evlsgsummul  21999  mhppwdeg  22037  psdpw  22057  ply1moncl  22157  coe1pwmul  22165  ply1coefsupp  22184  ply1coe  22185  gsummoncoe1  22195  lply1binomsc  22198  evls1gsummul  22212  evl1expd  22232  evl1gsummul  22247  evl1scvarpw  22250  evl1scvarpwval  22251  evl1gsummon  22252  evls1fpws  22256  rhmply1mon  22276  ringvcl  22287  mat1mhm  22371  scmatmhm  22421  m1detdiag  22484  mdetdiaglem  22485  m2detleiblem2  22515  mat2pmatmhm  22620  pmatcollpwscmatlem1  22676  mply1topmatcllem  22690  mply1topmatcl  22692  pm2mpghm  22703  pm2mpmhm  22707  monmat2matmon  22711  pm2mp  22712  chpscmatgsumbin  22731  chpscmatgsummon  22732  chfacfscmulcl  22744  chfacfscmul0  22745  chfacfpmmulcl  22748  chfacfpmmul0  22749  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  cayhamlem2  22771  cayhamlem4  22775  nrgtrg  24578  deg1pw  26026  idomrootle  26078  plypf1  26117  efsubm  26460  amgm  26901  wilthlem2  26979  wilthlem3  26980  dchrelbas3  27149  lgsqrlem2  27258  lgsqrlem3  27259  lgsqrlem4  27260  cntrcrng  33010  psgnid  33054  cnmsgn0g  33103  altgnsg  33106  isunit3  33192  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspn  33197  0ringcring  33203  domnprodn0  33226  rrgsubm  33234  znfermltl  33337  unitprodclb  33360  ringlsmss  33366  rprmdvdspow  33504  1arithidomlem1  33506  1arithidom  33508  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  zringfrac  33525  ressply1evls1  33534  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  gsummoncoe1fzo  33563  ply1degltdimlem  33618  ply1degltdim  33619  assarrginv  33632  evls1fldgencl  33665  rtelextdg2lem  33716  2sqr3minply  33770  cos9thpiminplylem6  33777  cos9thpiminply  33778  iistmd  33892  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p6  42102  evl1gprodd  42105  aks6d1c2lem3  42114  idomnnzpownz  42120  aks6d1c5lem3  42125  aks6d1c5lem2  42126  deg1pow  42129  aks6d1c6lem1  42158  aks6d1c6lem2  42159  aks5lem2  42175  aks5lem3a  42177  domnexpgn0cl  42511  abvexp  42520  fidomncyc  42523  evlsvvvallem  42549  evlsvvval  42551  evlsexpval  42555  evlselv  42575  mhphf  42585  hbtlem4  43115  mon1psubm  43188  amgm2d  44187  amgm3d  44188  amgm4d  44189  invginvrid  48355  ply1mulgsumlem4  48378  ply1mulgsum  48379  amgmw2d  49793