Theorem ringmgp 18599

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ‘cfv 5926  (class class class)co 6690  Basecbs 15904  +_gcplusg 15988  ._rcmulr 15989  Mndcmnd 17341  Grpcgrp 17469  mulGrpcmgp 18535  Ringcrg 18593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-ring 18595

This theorem is referenced by:  mgpf  18605  ringcl  18607  iscrng2  18609  ringass  18610  ringideu  18611  ringidcl  18614  ringidmlem  18616  ringsrg  18635  unitsubm  18716  dfrhm2  18765  isrhm2d  18776  idrhm  18779  pwsco1rhm  18786  pwsco2rhm  18787  subrgcrng  18832  subrgsubm  18841  issubrg3  18856  cntzsubr  18860  pwsdiagrhm  18861  assamulgscmlem2  19397  psrcrng  19461  mplcoe3  19514  mplcoe5lem  19515  mplcoe5  19516  ply1moncl  19689  coe1pwmul  19697  ply1coefsupp  19713  ply1coe  19714  gsummoncoe1  19722  lply1binomsc  19725  evls1gsummul  19738  evl1expd  19757  evl1gsummul  19772  evl1scvarpw  19775  evl1scvarpwval  19776  evl1gsummon  19777  cnfldexp  19827  expmhm  19863  nn0srg  19864  rge0srg  19865  ringvcl  20252  mat1mhm  20338  scmatmhm  20388  m1detdiag  20451  mdetdiaglem  20452  m2detleiblem2  20482  mat2pmatmhm  20586  pmatcollpwscmatlem1  20642  mply1topmatcllem  20656  mply1topmatcl  20658  pm2mpghm  20669  pm2mpmhm  20673  monmat2matmon  20677  pm2mp  20678  chpscmatgsumbin  20697  chpscmatgsummon  20698  chfacfscmulcl  20710  chfacfscmul0  20711  chfacfpmmulcl  20714  chfacfpmmul0  20715  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cayhamlem2  20737  cayhamlem4  20741  nrgtrg  22541  deg1pw  23925  plypf1  24013  efsubm  24342  amgm  24762  wilthlem2  24840  wilthlem3  24841  dchrelbas3  25008  lgsqrlem2  25117  lgsqrlem3  25118  lgsqrlem4  25119  psgnid  29975  iistmd  30076  hbtlem4  38013  subrgacs  38087  idomrootle  38090  isdomn3  38099  mon1psubm  38101  amgm2d  38818  amgm3d  38819  amgm4d  38820  c0rhm  42237  c0rnghm  42238  lidlmsgrp  42251  invginvrid  42473  ply1mulgsumlem4  42502  ply1mulgsum  42503  amgmw2d  42878