MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringcl Structured version   Visualization version   GIF version

Theorem ringcl 19316
Description: Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
ringcl.b 𝐵 = (Base‘𝑅)
ringcl.t · = (.r𝑅)
Assertion
Ref Expression
ringcl ((𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Proof of Theorem ringcl
StepHypRef Expression
1 eqid 2824 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
21ringmgp 19305 . 2 (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3 ringcl.b . . . 4 𝐵 = (Base‘𝑅)
41, 3mgpbas 19247 . . 3 𝐵 = (Base‘(mulGrp‘𝑅))
5 ringcl.t . . . 4 · = (.r𝑅)
61, 5mgpplusg 19245 . . 3 · = (+g‘(mulGrp‘𝑅))
74, 6mndcl 17921 . 2 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
82, 7syl3an1 1160 1 ((𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2115  cfv 6345  (class class class)co 7151  Basecbs 16485  .rcmulr 16568  Mndcmnd 17913  mulGrpcmgp 19241  Ringcrg 19299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-iun 4907  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7577  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11637  df-2 11699  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-plusg 16580  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-mgp 19242  df-ring 19301
This theorem is referenced by:  ringlz  19342  ringrz  19343  ringnegl  19349  rngnegr  19350  ringmneg1  19351  ringmneg2  19352  ringm2neg  19353  ringsubdi  19354  rngsubdir  19355  mulgass2  19356  ringlghm  19359  ringrghm  19360  gsumdixp  19364  prdsmulrcl  19366  imasring  19374  qusring2  19375  opprring  19386  dvdsrcl2  19405  dvdsrtr  19407  dvdsrmul1  19408  dvrcl  19441  dvrass  19445  irredrmul  19462  isdrngd  19529  subrgmcl  19549  abvtrivd  19613  srngmul  19631  issrngd  19634  idsrngd  19635  lmodmcl  19648  lmodprop2d  19698  rmodislmodlem  19703  prdslmodd  19743  sralmod  19961  2idlcpbl  20009  qusrhm  20012  quscrng  20015  frlmphl  20479  assa2ass  20561  assapropd  20567  ascldimul  20582  ascldimulOLD  20583  psrmulcllem  20634  psrvscacl  20640  psrlmod  20648  psrlidm  20650  psrridm  20651  psrass1  20652  psrdi  20653  psrdir  20654  psrass23l  20655  psrcom  20656  psrass23  20657  mplmonmul  20713  mplmon2mul  20749  mplind  20750  evlslem2  20760  evlslem3  20761  evlslem6  20762  evlslem1  20763  mpfind  20788  psropprmul  20876  coe1mul2  20907  coe1tmmul2  20914  coe1tmmul  20915  evl1muld  20976  mamucl  21015  mamuass  21016  mamudi  21017  mamudir  21018  mamuvs1  21019  mamuvs2  21020  mamulid  21055  mamurid  21056  madetsmelbas  21078  madetsmelbas2  21079  mat1dimscm  21089  mat1dimmul  21090  mat1mhm  21098  dmatmul  21111  dmatmulcl  21114  scmatscmiddistr  21122  scmatscm  21127  scmatmulcl  21132  smatvscl  21138  scmatmhm  21148  mavmulcl  21161  mavmulass  21163  mdetleib2  21202  mdetf  21209  mdetrlin  21216  mdetrsca  21217  mdetrsca2  21218  mdetralt  21222  mdetero  21224  mdetuni0  21235  mdetmul  21237  m2detleib  21245  madugsum  21257  madulid  21259  cpmatmcllem  21332  cpmatmcl  21333  mat2pmatmul  21345  decpmatmullem  21385  decpmatmul  21386  decpmatmulsumfsupp  21387  pm2mpmhmlem1  21432  pm2mpmhmlem2  21433  chfacfisf  21468  chfacfscmulgsum  21474  chfacfpmmulcl  21475  chfacfpmmulgsum  21478  chfacfpmmulgsum2  21479  cayhamlem1  21480  cpmadugsumlemF  21490  cayhamlem4  21502  nrgdsdi  23280  nrgdsdir  23281  nrginvrcnlem  23306  mdegmullem  24688  coe1mul3  24709  deg1mul2  24724  deg1mul3  24725  deg1mul3le  24726  ply1domn  24733  ply1divmo  24745  ply1divex  24746  uc1pmon1p  24761  r1pcl  24767  r1pid  24769  dvdsq1p  24770  dvdsr1p  24771  ply1rem  24773  dchrelbas3  25831  dchrmulcl  25842  dchrinv  25854  abvcxp  26208  freshmansdream  30901  frobrhm  30902  rdivmuldivd  30905  ornglmulle  30921  orngrmulle  30922  ornglmullt  30923  orngrmullt  30924  orngmullt  30925  isprmidlc  31016  qsidomlem1  31018  qsidomlem2  31019  mxidlprm  31030  drgextlsp  31064  fedgmullem1  31093  fedgmullem2  31094  fedgmul  31095  extdg1id  31121  mdetpmtr1  31156  matunitlindflem1  35025  matunitlindflem2  35026  lflnegcl  36343  lflvscl  36345  lkrlsp  36370  ldualvsass  36409  lclkrlem2m  38787  lclkrlem2o  38789  lclkrlem2p  38790  lcfrlem2  38811  lcfrlem3  38812  lcfrlem29  38839  mapdpglem30  38970  hdmapglem7  39197  prjspertr  39543  hbtlem2  40012  mendlmod  40081  mendassa  40082  isdomn3  40092  mon1psubm  40094  deg1mhm  40095  mnringmulrcld  40884  lidldomn1  44498  ply1mulgsum  44751  lincscm  44792  lincscmcl  44794  lincresunitlem2  44838  lmod1lem4  44852
  Copyright terms: Public domain W3C validator