Theorem ringmgp 19704

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 2738	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
3		eqid 2738	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2738	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 19702	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp2bi 1144	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  ._rcmulr 16889  Mndcmnd 18300  Grpcgrp 18492  mulGrpcmgp 19635  Ringcrg 19698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-ring 19700

This theorem is referenced by:  mgpf  19713  ringcl  19715  iscrng2  19717  ringass  19718  ringideu  19719  ringidcl  19722  ringidmlem  19724  ringsrg  19743  unitsubm  19827  dfrhm2  19876  isrhm2d  19887  idrhm  19890  pwsco1rhm  19897  pwsco2rhm  19898  subrgcrng  19943  subrgsubm  19952  issubrg3  19967  cntzsubr  19972  pwsdiagrhm  19973  subrgacs  19983  cnfldexp  20543  expmhm  20579  nn0srg  20580  rge0srg  20581  assamulgscmlem2  21014  psrcrng  21092  mplcoe3  21149  mplcoe5lem  21150  mplcoe5  21151  evlsgsummul  21212  mhppwdeg  21250  ply1moncl  21352  coe1pwmul  21360  ply1coefsupp  21376  ply1coe  21377  gsummoncoe1  21385  lply1binomsc  21388  evls1gsummul  21401  evl1expd  21421  evl1gsummul  21436  evl1scvarpw  21439  evl1scvarpwval  21440  evl1gsummon  21441  ringvcl  21457  mat1mhm  21541  scmatmhm  21591  m1detdiag  21654  mdetdiaglem  21655  m2detleiblem2  21685  mat2pmatmhm  21790  pmatcollpwscmatlem1  21846  mply1topmatcllem  21860  mply1topmatcl  21862  pm2mpghm  21873  pm2mpmhm  21877  monmat2matmon  21881  pm2mp  21882  chpscmatgsumbin  21901  chpscmatgsummon  21902  chfacfscmulcl  21914  chfacfscmul0  21915  chfacfpmmulcl  21918  chfacfpmmul0  21919  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cayhamlem2  21941  cayhamlem4  21945  nrgtrg  23760  deg1pw  25190  plypf1  25278  efsubm  25612  amgm  26045  wilthlem2  26123  wilthlem3  26124  dchrelbas3  26291  lgsqrlem2  26400  lgsqrlem3  26401  lgsqrlem4  26402  cntrcrng  31224  psgnid  31266  cnmsgn0g  31315  altgnsg  31318  freshmansdream  31386  frobrhm  31387  znfermltl  31464  ringlsmss  31485  iistmd  31754  pwspjmhmmgpd  40192  pwsexpg  40193  evlsbagval  40198  evlsexpval  40199  mhphf  40208  hbtlem4  40867  idomrootle  40936  isdomn3  40945  mon1psubm  40947  amgm2d  41698  amgm3d  41699  amgm4d  41700  c0rhm  45358  c0rnghm  45359  lidlmsgrp  45372  invginvrid  45591  ply1mulgsumlem4  45618  ply1mulgsum  45619  amgmw2d  46394