MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rngcl Structured version   Unicode version

Theorem rngcl 16780
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
rngcl.b  |-  B  =  ( Base `  R
)
rngcl.t  |-  .x.  =  ( .r `  R )
Assertion
Ref Expression
rngcl  |-  ( ( R  e.  Ring  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .x.  Y )  e.  B )

Proof of Theorem rngcl
StepHypRef Expression
1 eqid 2454 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21rngmgp 16773 . 2  |-  ( R  e.  Ring  ->  (mulGrp `  R )  e.  Mnd )
3 rngcl.b . . . 4  |-  B  =  ( Base `  R
)
41, 3mgpbas 16718 . . 3  |-  B  =  ( Base `  (mulGrp `  R ) )
5 rngcl.t . . . 4  |-  .x.  =  ( .r `  R )
61, 5mgpplusg 16716 . . 3  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
74, 6mndcl 15538 . 2  |-  ( ( (mulGrp `  R )  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .x.  Y )  e.  B )
82, 7syl3an1 1252 1  |-  ( ( R  e.  Ring  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .x.  Y )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965    = wceq 1370    e. wcel 1758   ` cfv 5525  (class class class)co 6199   Basecbs 14291   .rcmulr 14357   Mndcmnd 15527  mulGrpcmgp 16712   Ringcrg 16767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-om 6586  df-recs 6941  df-rdg 6975  df-er 7210  df-en 7420  df-dom 7421  df-sdom 7422  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-nn 10433  df-2 10490  df-ndx 14294  df-slot 14295  df-base 14296  df-sets 14297  df-plusg 14369  df-mnd 15533  df-mgp 16713  df-rng 16769
This theorem is referenced by:  rnglz  16803  rngrz  16804  rngnegl  16807  rngnegr  16808  rngmneg1  16809  rngmneg2  16810  rngm2neg  16811  rngsubdi  16812  rngsubdir  16813  mulgass2  16814  rnglghm  16815  rngrghm  16816  gsumdixpOLD  16822  gsumdixp  16823  prdsmulrcl  16825  imasrng  16833  divsrng2  16834  opprrng  16845  dvdsrcl2  16864  dvdsrtr  16866  dvdsrmul1  16867  dvrcl  16900  dvrass  16904  irredrmul  16921  isdrngd  16979  subrgmcl  16999  abvtrivd  17047  srngmul  17065  issrngd  17068  idsrngd  17069  lmodmcl  17082  lmodprop2d  17129  prdslmodd  17172  sralmod  17390  2idlcpbl  17438  divsrhm  17441  divscrng  17444  assapropd  17520  asclrhm  17534  psrmulcllem  17580  psrvscacl  17586  psrlmod  17594  psrlidm  17596  psrlidmOLD  17597  psrridm  17598  psrridmOLD  17599  psrass1  17600  psrdi  17601  psrdir  17602  psrass23l  17603  psrcom  17604  psrass23  17605  mplmonmul  17666  mplmon2mul  17706  mplind  17707  evlslem2  17720  evlslem6  17721  evlslem6OLD  17722  evlslem3  17723  evlslem1  17724  mpfind  17745  psropprmul  17815  coe1mul2  17845  coe1tmmul2  17852  coe1tmmul  17853  evl1muld  17901  frlmphl  18330  mamucl  18425  mamulid  18428  mamurid  18429  mamuass  18430  mamudi  18431  mamudir  18432  mamuvs1  18433  mamuvs2  18434  madetsmelbas  18475  madetsmelbas2  18476  mavmulcl  18484  mavmulass  18486  mdetleib2  18525  mdetf  18532  mdetrlin  18539  mdetrsca  18540  mdetrsca2  18541  mdetralt  18545  mdetero  18547  mdetuni0  18558  mdetmul  18560  m2detleib  18568  madugsum  18580  madulid  18582  nrgdsdi  20377  nrgdsdir  20378  nrginvrcnlem  20402  mdegmullem  21681  coe1mul3  21703  deg1mul2  21718  deg1mul3  21719  deg1mul3le  21720  ply1domn  21727  ply1divmo  21739  ply1divex  21740  uc1pmon1p  21755  r1pcl  21761  r1pid  21763  dvdsq1p  21764  dvdsr1p  21765  ply1rem  21767  dchrelbas3  22709  dchrmulcl  22720  dchrinv  22732  abvcxp  22996  rdivmuldivd  26403  ornglmulle  26417  orngrmulle  26418  ornglmullt  26419  orngrmullt  26420  orngmullt  26421  hbtlem2  29627  mendlmod  29697  mendassa  29698  isdomn3  29719  mon1psubm  29721  deg1mhm  29722  assa2ass  30973  ply1mulgsum  31001  mat1dimscm  31036  mat1dimmul  31037  dmatmul  31041  dmatmulcl  31044  scmatmulcl  31051  lincscm  31082  lincscmcl  31084  lincresunitlem2  31128  lmod1lem4  31150  cpmatmcllem  31193  cpmatmcl  31194  mat2pmatmul  31206  decpmatmullem  31244  decpmatmul  31245  decpmatmulsumfsupp  31246  pm2mpmhmlem1  31290  pm2mpmhmlem2  31291  chfacfisf  31325  chfacfscmulgsum  31331  chfacfpmmulcl  31332  chfacfpmmulgsum  31335  chfacfpmmulgsum2  31336  cayhamlem1  31337  cpmadugsumlemF  31347  cayhamlem4  31360  lflnegcl  33043  lflvscl  33045  lkrlsp  33070  ldualvsass  33109  lclkrlem2m  35487  lclkrlem2o  35489  lclkrlem2p  35490  lcfrlem2  35511  lcfrlem3  35512  lcfrlem29  35539  mapdpglem30  35670  hdmapglem7  35900
  Copyright terms: Public domain W3C validator