Theorem ringmgp 20495

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 2763	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2763	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2763	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20493	. 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 2147  ∀wral 3080  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  ._rcmulr 17458  Mndcmnd 18952  Grpcgrp 19173  mulGrpcmgp 20390  Ringcrg 20489

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-ring 20491

This theorem is used by:  mgpf  20505  ringcl  20507  iscrng2  20509  ringass  20510  ringideu  20511  ringidcl  20524  ringidmlem  20527  dfring2  20547  ringsrg  20558  pwspjmhmmgpd  20587  pwsexpg  20588  unitsubm  20646  dfrhm2  20734  isrhm2d  20751  idrhm  20755  pwsco1rhm  20771  pwsco2rhm  20772  c0rhm  20816  c0rnghm  20817  subrgcrng  20857  subrgsubm  20867  issubrg3  20882  cntzsubr  20888  pwsdiagrhm  20889  isdomn3  20996  isdrng3lem1  21035  subrgacs  21087  prmidlsubm  21673  cnfldexp  21741  expmhm  21772  nn0srg  21773  rge0srg  21774  fermltlchr  21865  freshmansdream  21910  frobrhm  21911  assamulgscmlem2  22238  psrcrng  22309  mplcoe3  22377  mplcoe5lem  22378  mplcoe5  22379  evlsvvvallem  22430  evlsvvval  22432  evlsgsummul  22436  evlsexpval  22467  mhppwdeg  22501  psdpw  22521  ply1moncl  22620  coe1pwmul  22628  ply1coefsupp  22645  ply1coe  22646  gsummoncoe1  22656  lply1binomsc  22659  evls1gsummul  22673  evl1expd  22693  evl1gsummul  22708  evl1scvarpw  22711  evl1scvarpwval  22712  evl1gsummon  22713  evls1fpws  22717  rhmply1mon  22734  ringvcl  22745  mat1mhm  22829  scmatmhm  22879  m1detdiag  22942  mdetdiaglem  22943  m2detleiblem2  22973  mat2pmatmhm  23081  pmatcollpwscmatlem1  23137  mply1topmatcllem  23151  mply1topmatcl  23153  pm2mpghm  23164  pm2mpmhm  23168  monmat2matmon  23172  pm2mp  23173  chpscmatgsumbin  23192  chpscmatgsummon  23193  chfacfscmulcl  23205  chfacfscmul0  23206  chfacfpmmulcl  23209  chfacfpmmul0  23210  chfacfpmmulgsum2  23213  cayhamlem1  23214  cpmadugsumlemB  23222  cpmadugsumlemC  23223  cpmadugsumlemF  23224  cayhamlem2  23232  cayhamlem4  23236  nrgtrg  25039  deg1pw  26469  idomrootle  26521  plypf1  26561  efsubm  26909  amgm  27348  wilthlem2  27426  wilthlem3  27427  dchrelbas3  27595  lgsqrlem2  27704  lgsqrlem3  27705  lgsqrlem4  27706  cntrcrng  33712  psgnid  33728  cnmsgn0g  33777  altgnsg  33780  ringm1expp1  33864  isunit3  33871  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnlem3  33875  elrgspnlem4  33876  elrgspn  33877  0ringcring  33883  domnprodn0  33909  rrgsubm  33915  znfermltl  33992  unitprodclb  34014  ringlsmss  34018  rprmdvdspow  34135  1arithidomlem1  34137  1arithidom  34139  1arithufdlem2  34147  1arithufdlem3  34148  1arithufdlem4  34149  zringfrac  34156  ressply1evls1  34167  evl1deg1  34178  evl1deg2  34179  evl1deg3  34180  evls1monply1  34181  ply1coedeg  34191  gsummoncoe1fzo  34199  vietalem  34281  ply1degltdimlem  34324  ply1degltdim  34325  assarrginv  34338  evls1fldgencl  34372  extdgfialglem1  34394  extdgfialglem2  34395  rtelextdg2lem  34428  2sqr3minply  34482  cos9thpiminplylem6  34489  cos9thpiminply  34490  iistmd  34604  aks6d1c1p2  43351  aks6d1c1p3  43352  aks6d1c1p6  43356  evl1gprodd  43359  aks6d1c2lem3  43368  idomnnzpownz  43374  aks6d1c5lem3  43379  aks6d1c5lem2  43380  deg1pow  43383  aks6d1c6lem1  43412  aks6d1c6lem2  43413  aks5lem2  43429  aks5lem3a  43431  domnexpgn0cl  43777  abvexp  43789  fidomncyc  43792  evlselv  43810  mhphf  43818  hbtlem4  44320  mon1psubm  44393  amgm2d  45390  amgm3d  45391  amgm4d  45392  invginvrid  49684  ply1mulgsumlem4  49706  ply1mulgsum  49707  amgmw2d  51269