Theorem ringmgp 19789

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 19787	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp2bi 1145	1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ‘cfv 6433  (class class class)co 7275  Basecbs 16912  +_gcplusg 16962  ._rcmulr 16963  Mndcmnd 18385  Grpcgrp 18577  mulGrpcmgp 19720  Ringcrg 19783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-ring 19785

This theorem is referenced by:  mgpf  19798  ringcl  19800  iscrng2  19802  ringass  19803  ringideu  19804  ringidcl  19807  ringidmlem  19809  ringsrg  19828  unitsubm  19912  dfrhm2  19961  isrhm2d  19972  idrhm  19975  pwsco1rhm  19982  pwsco2rhm  19983  subrgcrng  20028  subrgsubm  20037  issubrg3  20052  cntzsubr  20057  pwsdiagrhm  20058  subrgacs  20068  cnfldexp  20631  expmhm  20667  nn0srg  20668  rge0srg  20669  assamulgscmlem2  21104  psrcrng  21182  mplcoe3  21239  mplcoe5lem  21240  mplcoe5  21241  evlsgsummul  21302  mhppwdeg  21340  ply1moncl  21442  coe1pwmul  21450  ply1coefsupp  21466  ply1coe  21467  gsummoncoe1  21475  lply1binomsc  21478  evls1gsummul  21491  evl1expd  21511  evl1gsummul  21526  evl1scvarpw  21529  evl1scvarpwval  21530  evl1gsummon  21531  ringvcl  21547  mat1mhm  21633  scmatmhm  21683  m1detdiag  21746  mdetdiaglem  21747  m2detleiblem2  21777  mat2pmatmhm  21882  pmatcollpwscmatlem1  21938  mply1topmatcllem  21952  mply1topmatcl  21954  pm2mpghm  21965  pm2mpmhm  21969  monmat2matmon  21973  pm2mp  21974  chpscmatgsumbin  21993  chpscmatgsummon  21994  chfacfscmulcl  22006  chfacfscmul0  22007  chfacfpmmulcl  22010  chfacfpmmul0  22011  chfacfpmmulgsum2  22014  cayhamlem1  22015  cpmadugsumlemB  22023  cpmadugsumlemC  22024  cpmadugsumlemF  22025  cayhamlem2  22033  cayhamlem4  22037  nrgtrg  23854  deg1pw  25285  plypf1  25373  efsubm  25707  amgm  26140  wilthlem2  26218  wilthlem3  26219  dchrelbas3  26386  lgsqrlem2  26495  lgsqrlem3  26496  lgsqrlem4  26497  cntrcrng  31322  psgnid  31364  cnmsgn0g  31413  altgnsg  31416  freshmansdream  31484  frobrhm  31485  znfermltl  31562  ringlsmss  31583  iistmd  31852  pwspjmhmmgpd  40267  pwsexpg  40268  evlsbagval  40275  evlsexpval  40276  mhphf  40285  hbtlem4  40951  idomrootle  41020  isdomn3  41029  mon1psubm  41031  amgm2d  41809  amgm3d  41810  amgm4d  41811  c0rhm  45470  c0rnghm  45471  lidlmsgrp  45484  invginvrid  45703  ply1mulgsumlem4  45730  ply1mulgsum  45731  amgmw2d  46508