Theorem ringmgp 20445

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 2761	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2761	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2761	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20443	. 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 2145  ∀wral 3077  ‘cfv 6531  (class class class)co 7412  Basecbs 17367  +_gcplusg 17408  ._rcmulr 17409  Mndcmnd 18903  Grpcgrp 19124  mulGrpcmgp 20340  Ringcrg 20439

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-ring 20441

This theorem is used by:  mgpf  20455  ringcl  20457  iscrng2  20459  ringass  20460  ringideu  20461  ringidcl  20474  ringidmlem  20477  dfring2  20497  ringsrg  20508  pwspjmhmmgpd  20537  pwsexpg  20538  unitsubm  20596  dfrhm2  20684  isrhm2d  20701  idrhm  20705  pwsco1rhm  20721  pwsco2rhm  20722  c0rhm  20766  c0rnghm  20767  subrgcrng  20807  subrgsubm  20817  issubrg3  20832  cntzsubr  20838  pwsdiagrhm  20839  isdomn3  20946  isdrng3lem1  20985  subrgacs  21037  prmidlsubm  21623  cnfldexp  21691  expmhm  21722  nn0srg  21723  rge0srg  21724  fermltlchr  21815  freshmansdream  21860  frobrhm  21861  assamulgscmlem2  22188  psrcrng  22259  mplcoe3  22327  mplcoe5lem  22328  mplcoe5  22329  evlsvvvallem  22380  evlsvvval  22382  evlsgsummul  22386  evlsexpval  22417  mhppwdeg  22451  psdpw  22471  ply1moncl  22570  coe1pwmul  22578  ply1coefsupp  22595  ply1coe  22596  gsummoncoe1  22606  lply1binomsc  22609  evls1gsummul  22623  evl1expd  22643  evl1gsummul  22658  evl1scvarpw  22661  evl1scvarpwval  22662  evl1gsummon  22663  evls1fpws  22667  rhmply1mon  22684  ringvcl  22695  mat1mhm  22779  scmatmhm  22829  m1detdiag  22892  mdetdiaglem  22893  m2detleiblem2  22923  mat2pmatmhm  23031  pmatcollpwscmatlem1  23087  mply1topmatcllem  23101  mply1topmatcl  23103  pm2mpghm  23114  pm2mpmhm  23118  monmat2matmon  23122  pm2mp  23123  chpscmatgsumbin  23142  chpscmatgsummon  23143  chfacfscmulcl  23155  chfacfscmul0  23156  chfacfpmmulcl  23159  chfacfpmmul0  23160  chfacfpmmulgsum2  23163  cayhamlem1  23164  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  cayhamlem2  23182  cayhamlem4  23186  nrgtrg  24989  deg1pw  26419  idomrootle  26471  plypf1  26511  efsubm  26861  amgm  27300  wilthlem2  27378  wilthlem3  27379  dchrelbas3  27547  lgsqrlem2  27656  lgsqrlem3  27657  lgsqrlem4  27658  cntrcrng  33624  psgnid  33640  cnmsgn0g  33689  altgnsg  33692  ringm1expp1  33776  isunit3  33783  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem3  33787  elrgspnlem4  33788  elrgspn  33789  0ringcring  33795  domnprodn0  33821  rrgsubm  33827  znfermltl  33904  unitprodclb  33926  ringlsmss  33930  rprmdvdspow  34047  1arithidomlem1  34049  1arithidom  34051  1arithufdlem2  34059  1arithufdlem3  34060  1arithufdlem4  34061  zringfrac  34068  ressply1evls1  34079  evl1deg1  34090  evl1deg2  34091  evl1deg3  34092  evls1monply1  34093  ply1coedeg  34103  gsummoncoe1fzo  34111  vietalem  34193  ply1degltdimlem  34236  ply1degltdim  34237  assarrginv  34250  evls1fldgencl  34284  extdgfialglem1  34306  extdgfialglem2  34307  rtelextdg2lem  34340  2sqr3minply  34394  cos9thpiminplylem6  34401  cos9thpiminply  34402  iistmd  34516  aks6d1c1p2  43127  aks6d1c1p3  43128  aks6d1c1p6  43132  evl1gprodd  43135  aks6d1c2lem3  43144  idomnnzpownz  43150  aks6d1c5lem3  43155  aks6d1c5lem2  43156  deg1pow  43159  aks6d1c6lem1  43188  aks6d1c6lem2  43189  aks5lem2  43205  aks5lem3a  43207  domnexpgn0cl  43549  abvexp  43558  fidomncyc  43561  evlselv  43579  mhphf  43587  hbtlem4  44086  mon1psubm  44159  amgm2d  45157  amgm3d  45158  amgm4d  45159  invginvrid  49423  ply1mulgsumlem4  49445  ply1mulgsum  49446  amgmw2d  50933