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

Theorem rngcl 17013
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 2467 . . 3  |-  (mulGrp `  R )  =  (mulGrp `  R )
21rngmgp 17006 . 2  |-  ( R  e.  Ring  ->  (mulGrp `  R )  e.  Mnd )
3 rngcl.b . . . 4  |-  B  =  ( Base `  R
)
41, 3mgpbas 16949 . . 3  |-  B  =  ( Base `  (mulGrp `  R ) )
5 rngcl.t . . . 4  |-  .x.  =  ( .r `  R )
61, 5mgpplusg 16947 . . 3  |-  .x.  =  ( +g  `  (mulGrp `  R ) )
74, 6mndcl 15737 . 2  |-  ( ( (mulGrp `  R )  e.  Mnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .x.  Y )  e.  B )
82, 7syl3an1 1261 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 973    = wceq 1379    e. wcel 1767   ` cfv 5588  (class class class)co 6284   Basecbs 14490   .rcmulr 14556   Mndcmnd 15726  mulGrpcmgp 16943   Ringcrg 17000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-recs 7042  df-rdg 7076  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-2 10594  df-ndx 14493  df-slot 14494  df-base 14495  df-sets 14496  df-plusg 14568  df-mnd 15732  df-mgp 16944  df-rng 17002
This theorem is referenced by:  rnglz  17036  rngrz  17037  rngnegl  17041  rngnegr  17042  rngmneg1  17043  rngmneg2  17044  rngm2neg  17045  rngsubdi  17046  rngsubdir  17047  mulgass2  17048  rnglghm  17051  rngrghm  17052  gsumdixpOLD  17058  gsumdixp  17059  prdsmulrcl  17061  imasrng  17069  divsrng2  17070  opprrng  17081  dvdsrcl2  17100  dvdsrtr  17102  dvdsrmul1  17103  dvrcl  17136  dvrass  17140  irredrmul  17157  isdrngd  17221  subrgmcl  17241  abvtrivd  17289  srngmul  17307  issrngd  17310  idsrngd  17311  lmodmcl  17324  lmodprop2d  17372  prdslmodd  17415  sralmod  17633  2idlcpbl  17681  divsrhm  17684  divscrng  17687  assa2ass  17770  assapropd  17775  asclrhm  17790  psrmulcllem  17839  psrvscacl  17845  psrlmod  17853  psrlidm  17855  psrlidmOLD  17856  psrridm  17857  psrridmOLD  17858  psrass1  17859  psrdi  17860  psrdir  17861  psrass23l  17862  psrcom  17863  psrass23  17864  mplmonmul  17925  mplmon2mul  17965  mplind  17966  evlslem2  17979  evlslem6  17980  evlslem6OLD  17981  evlslem3  17982  evlslem1  17983  mpfind  18004  psropprmul  18078  coe1mul2  18109  coe1tmmul2  18116  coe1tmmul  18117  evl1muld  18178  frlmphl  18607  mamucl  18698  mamuass  18699  mamudi  18700  mamudir  18701  mamuvs1  18702  mamuvs2  18703  mamulid  18738  mamurid  18739  madetsmelbas  18761  madetsmelbas2  18762  mat1dimscm  18772  mat1dimmul  18773  mat1mhm  18781  dmatmul  18794  dmatmulcl  18797  scmatscmiddistr  18805  scmatscm  18810  scmatmulcl  18815  smatvscl  18821  scmatmhm  18831  mavmulcl  18844  mavmulass  18846  mdetleib2  18885  mdetf  18892  mdetrlin  18899  mdetrsca  18900  mdetrsca2  18901  mdetralt  18905  mdetero  18907  mdetuni0  18918  mdetmul  18920  m2detleib  18928  madugsum  18940  madulid  18942  cpmatmcllem  19014  cpmatmcl  19015  mat2pmatmul  19027  decpmatmullem  19067  decpmatmul  19068  decpmatmulsumfsupp  19069  pm2mpmhmlem1  19114  pm2mpmhmlem2  19115  chfacfisf  19150  chfacfscmulgsum  19156  chfacfpmmulcl  19157  chfacfpmmulgsum  19160  chfacfpmmulgsum2  19161  cayhamlem1  19162  cpmadugsumlemF  19172  cayhamlem4  19184  nrgdsdi  20937  nrgdsdir  20938  nrginvrcnlem  20962  mdegmullem  22241  coe1mul3  22263  deg1mul2  22278  deg1mul3  22279  deg1mul3le  22280  ply1domn  22287  ply1divmo  22299  ply1divex  22300  uc1pmon1p  22315  r1pcl  22321  r1pid  22323  dvdsq1p  22324  dvdsr1p  22325  ply1rem  22327  dchrelbas3  23269  dchrmulcl  23280  dchrinv  23292  abvcxp  23556  rdivmuldivd  27472  ornglmulle  27486  orngrmulle  27487  ornglmullt  27488  orngrmullt  27489  orngmullt  27490  hbtlem2  30705  mendlmod  30775  mendassa  30776  isdomn3  30797  mon1psubm  30799  deg1mhm  30800  ply1mulgsum  32089  lincscm  32130  lincscmcl  32132  lincresunitlem2  32176  lmod1lem4  32190  lflnegcl  33890  lflvscl  33892  lkrlsp  33917  ldualvsass  33956  lclkrlem2m  36334  lclkrlem2o  36336  lclkrlem2p  36337  lcfrlem2  36358  lcfrlem3  36359  lcfrlem29  36386  mapdpglem30  36517  hdmapglem7  36747
  Copyright terms: Public domain W3C validator