Theorem ringcl 19314

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

Step	Hyp	Ref	Expression
1		eqid 2824	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 19306	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 19248	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 19246	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 17922	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1159	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113  ‘cfv 6358  (class class class)co 7159  Basecbs 16486  ._rcmulr 16569  Mndcmnd 17914  mulGrpcmgp 19242  Ringcrg 19300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-cnex 10596  ax-resscn 10597  ax-1cn 10598  ax-icn 10599  ax-addcl 10600  ax-addrcl 10601  ax-mulcl 10602  ax-mulrcl 10603  ax-mulcom 10604  ax-addass 10605  ax-mulass 10606  ax-distr 10607  ax-i2m1 10608  ax-1ne0 10609  ax-1rid 10610  ax-rnegex 10611  ax-rrecex 10612  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615  ax-pre-ltadd 10616  ax-pre-mulgt0 10617

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7117  df-ov 7162  df-oprab 7163  df-mpo 7164  df-om 7584  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684  df-sub 10875  df-neg 10876  df-nn 11642  df-2 11703  df-ndx 16489  df-slot 16490  df-base 16492  df-sets 16493  df-plusg 16581  df-mgm 17855  df-sgrp 17904  df-mnd 17915  df-mgp 19243  df-ring 19302

This theorem is referenced by:  ringlz  19340  ringrz  19341  ringnegl  19347  rngnegr  19348  ringmneg1  19349  ringmneg2  19350  ringm2neg  19351  ringsubdi  19352  rngsubdir  19353  mulgass2  19354  ringlghm  19357  ringrghm  19358  gsumdixp  19362  prdsmulrcl  19364  imasring  19372  qusring2  19373  opprring  19384  dvdsrcl2  19403  dvdsrtr  19405  dvdsrmul1  19406  dvrcl  19439  dvrass  19443  irredrmul  19460  isdrngd  19530  subrgmcl  19550  abvtrivd  19614  srngmul  19632  issrngd  19635  idsrngd  19636  lmodmcl  19649  lmodprop2d  19699  rmodislmodlem  19704  prdslmodd  19744  sralmod  19962  2idlcpbl  20010  qusrhm  20013  quscrng  20016  assa2ass  20098  assapropd  20104  ascldimul  20119  ascldimulOLD  20120  psrmulcllem  20170  psrvscacl  20176  psrlmod  20184  psrlidm  20186  psrridm  20187  psrass1  20188  psrdi  20189  psrdir  20190  psrass23l  20191  psrcom  20192  psrass23  20193  mplmonmul  20248  mplmon2mul  20284  mplind  20285  evlslem2  20295  evlslem3  20296  evlslem6  20297  evlslem1  20298  mpfind  20323  psropprmul  20409  coe1mul2  20440  coe1tmmul2  20447  coe1tmmul  20448  evl1muld  20509  frlmphl  20928  mamucl  21013  mamuass  21014  mamudi  21015  mamudir  21016  mamuvs1  21017  mamuvs2  21018  mamulid  21053  mamurid  21054  madetsmelbas  21076  madetsmelbas2  21077  mat1dimscm  21087  mat1dimmul  21088  mat1mhm  21096  dmatmul  21109  dmatmulcl  21112  scmatscmiddistr  21120  scmatscm  21125  scmatmulcl  21130  smatvscl  21136  scmatmhm  21146  mavmulcl  21159  mavmulass  21161  mdetleib2  21200  mdetf  21207  mdetrlin  21214  mdetrsca  21215  mdetrsca2  21216  mdetralt  21220  mdetero  21222  mdetuni0  21233  mdetmul  21235  m2detleib  21243  madugsum  21255  madulid  21257  cpmatmcllem  21329  cpmatmcl  21330  mat2pmatmul  21342  decpmatmullem  21382  decpmatmul  21383  decpmatmulsumfsupp  21384  pm2mpmhmlem1  21429  pm2mpmhmlem2  21430  chfacfisf  21465  chfacfscmulgsum  21471  chfacfpmmulcl  21472  chfacfpmmulgsum  21475  chfacfpmmulgsum2  21476  cayhamlem1  21477  cpmadugsumlemF  21487  cayhamlem4  21499  nrgdsdi  23277  nrgdsdir  23278  nrginvrcnlem  23303  mdegmullem  24675  coe1mul3  24696  deg1mul2  24711  deg1mul3  24712  deg1mul3le  24713  ply1domn  24720  ply1divmo  24732  ply1divex  24733  uc1pmon1p  24748  r1pcl  24754  r1pid  24756  dvdsq1p  24757  dvdsr1p  24758  ply1rem  24760  dchrelbas3  25817  dchrmulcl  25828  dchrinv  25840  abvcxp  26194  freshmansdream  30863  rdivmuldivd  30866  ornglmulle  30882  orngrmulle  30883  ornglmullt  30884  orngrmullt  30885  orngmullt  30886  isprmidlc  30967  qsidomlem1  30969  qsidomlem2  30970  mxidlprm  30981  drgextlsp  31000  fedgmullem1  31029  fedgmullem2  31030  fedgmul  31031  extdg1id  31057  mdetpmtr1  31092  matunitlindflem1  34892  matunitlindflem2  34893  lflnegcl  36215  lflvscl  36217  lkrlsp  36242  ldualvsass  36281  lclkrlem2m  38659  lclkrlem2o  38661  lclkrlem2p  38662  lcfrlem2  38683  lcfrlem3  38684  lcfrlem29  38711  mapdpglem30  38842  hdmapglem7  39069  prjspertr  39261  hbtlem2  39730  mendlmod  39799  mendassa  39800  isdomn3  39810  mon1psubm  39812  deg1mhm  39813  lidldomn1  44199  ply1mulgsum  44451  lincscm  44492  lincscmcl  44494  lincresunitlem2  44538  lmod1lem4  44552