Theorem ringmgp 18553

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  +_gcplusg 15941  ._rcmulr 15942  Mndcmnd 17294  Grpcgrp 17422  mulGrpcmgp 18489  Ringcrg 18547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-ring 18549

This theorem is referenced by:  mgpf  18559  ringcl  18561  iscrng2  18563  ringass  18564  ringideu  18565  ringidcl  18568  ringidmlem  18570  ringsrg  18589  unitsubm  18670  dfrhm2  18717  isrhm2d  18728  idrhm  18731  pwsco1rhm  18738  pwsco2rhm  18739  subrgcrng  18784  subrgsubm  18793  issubrg3  18808  cntzsubr  18812  pwsdiagrhm  18813  assamulgscmlem2  19349  psrcrng  19413  mplcoe3  19466  mplcoe5lem  19467  mplcoe5  19468  ply1moncl  19641  coe1pwmul  19649  ply1coefsupp  19665  ply1coe  19666  gsummoncoe1  19674  lply1binomsc  19677  evls1gsummul  19690  evl1expd  19709  evl1gsummul  19724  evl1scvarpw  19727  evl1scvarpwval  19728  evl1gsummon  19729  cnfldexp  19779  expmhm  19815  nn0srg  19816  rge0srg  19817  ringvcl  20204  mat1mhm  20290  scmatmhm  20340  m1detdiag  20403  mdetdiaglem  20404  m2detleiblem2  20434  mat2pmatmhm  20538  pmatcollpwscmatlem1  20594  mply1topmatcllem  20608  mply1topmatcl  20610  pm2mpghm  20621  pm2mpmhm  20625  monmat2matmon  20629  pm2mp  20630  chpscmatgsumbin  20649  chpscmatgsummon  20650  chfacfscmulcl  20662  chfacfscmul0  20663  chfacfpmmulcl  20666  chfacfpmmul0  20667  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cayhamlem2  20689  cayhamlem4  20693  nrgtrg  22494  deg1pw  23880  plypf1  23968  efsubm  24297  amgm  24717  wilthlem2  24795  wilthlem3  24796  dchrelbas3  24963  lgsqrlem2  25072  lgsqrlem3  25073  lgsqrlem4  25074  psgnid  29847  iistmd  29948  hbtlem4  37696  subrgacs  37770  idomrootle  37773  isdomn3  37782  mon1psubm  37784  amgm2d  38501  amgm3d  38502  amgm4d  38503  c0rhm  41912  c0rnghm  41913  lidlmsgrp  41926  invginvrid  42148  ply1mulgsumlem4  42177  ply1mulgsum  42178  amgmw2d  42550