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

Theorem rngcl 16596
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 2435 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21rngmgp 16589 . 2  |-  ( R  e.  Ring  ->  (mulGrp `  R )  e.  Mnd )
3 rngcl.b . . . 4  |-  B  =  ( Base `  R
)
41, 3mgpbas 16573 . . 3  |-  B  =  ( Base `  (mulGrp `  R ) )
5 rngcl.t . . . 4  |-  .x.  =  ( .r `  R )
61, 5mgpplusg 16571 . . 3  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
74, 6mndcl 15405 . 2  |-  ( ( (mulGrp `  R )  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .x.  Y )  e.  B )
82, 7syl3an1 1246 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 960    = wceq 1364    e. wcel 1757   ` cfv 5408  (class class class)co 6082   Basecbs 14159   .rcmulr 14224   Mndcmnd 15394  mulGrpcmgp 16567   Ringcrg 16579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-recs 6820  df-rdg 6854  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-nn 10313  df-2 10370  df-ndx 14162  df-slot 14163  df-base 14164  df-sets 14165  df-plusg 14236  df-mnd 15400  df-mgp 16568  df-rng 16582
This theorem is referenced by:  rnglz  16619  rngrz  16620  rngnegl  16622  rngnegr  16623  rngmneg1  16624  rngmneg2  16625  rngm2neg  16626  rngsubdi  16627  rngsubdir  16628  mulgass2  16629  rnglghm  16630  rngrghm  16631  gsumdixpOLD  16637  gsumdixp  16638  prdsmulrcl  16640  imasrng  16648  divsrng2  16649  opprrng  16659  dvdsrcl2  16678  dvdsrtr  16680  dvdsrmul1  16681  dvrcl  16714  dvrass  16718  irredrmul  16735  isdrngd  16783  subrgmcl  16803  abvtrivd  16851  srngmul  16869  issrngd  16872  idsrngd  16873  lmodmcl  16886  lmodprop2d  16933  prdslmodd  16974  sralmod  17192  2idlcpbl  17240  divsrhm  17243  divscrng  17246  assapropd  17322  asclrhm  17336  psrmulcllem  17394  psrvscacl  17400  psrlmod  17408  psrlidm  17410  psrlidmOLD  17411  psrridm  17412  psrridmOLD  17413  psrass1  17414  psrdi  17415  psrdir  17416  psrcom  17417  psrass23  17418  mplmonmul  17479  mplmon2mul  17517  mplind  17518  evlslem2  17527  psropprmul  17593  coe1mul2  17623  coe1tmmul2  17629  coe1tmmul  17630  frlmphl  18050  mamucl  18145  mamulid  18148  mamurid  18149  mamuass  18150  mamudi  18151  mamudir  18152  mamuvs1  18153  mamuvs2  18154  madetsmelbas  18193  madetsmelbas2  18194  mavmulcl  18202  mavmulass  18204  mdetleib2  18243  mdetf  18250  mdetrlin  18253  mdetrsca  18254  mdetrsca2  18255  mdetralt  18258  mdetero  18260  mdetuni0  18271  mdetmul  18273  m2detleib  18281  madugsum  18293  madulid  18295  nrgdsdi  20090  nrgdsdir  20091  nrginvrcnlem  20115  evlslem6  21366  evlslem6OLD  21367  evlslem3  21368  evlslem1  21369  evl1muld  21389  mpfind  21398  mdegmullem  21436  coe1mul3  21458  deg1mul2  21473  deg1mul3  21474  deg1mul3le  21475  ply1domn  21482  ply1divmo  21494  ply1divex  21495  uc1pmon1p  21510  r1pcl  21516  r1pid  21518  dvdsq1p  21519  dvdsr1p  21520  ply1rem  21522  dchrelbas3  22464  dchrmulcl  22475  dchrinv  22487  abvcxp  22751  rdivmuldivd  26114  ornglmulle  26128  orngrmulle  26129  ornglmullt  26130  orngrmullt  26131  orngmullt  26132  hbtlem2  29327  mendlmod  29397  mendassa  29398  isdomn3  29419  mon1psubm  29421  deg1mhm  29422  assa2ass  30634  psrass23l  30635  mat1dimscm  30662  mat1dimmul  30663  dmatmul  30667  dmatmulcl  30670  scmatmulcl  30677  lincscm  30713  lincscmcl  30715  lincresunitlem2  30759  lmod1lem4  30781  lflnegcl  32333  lflvscl  32335  lkrlsp  32360  ldualvsass  32399  lclkrlem2m  34777  lclkrlem2o  34779  lclkrlem2p  34780  lcfrlem2  34801  lcfrlem3  34802  lcfrlem29  34829  mapdpglem30  34960  hdmapglem7  35190
  Copyright terms: Public domain W3C validator