Theorem ringcl 19715

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 2738	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 19704	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 19641	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 19639	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18308	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1161	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  ._rcmulr 16889  Mndcmnd 18300  mulGrpcmgp 19635  Ringcrg 19698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-2 11966  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-plusg 16901  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-mgp 19636  df-ring 19700

This theorem is referenced by:  ringlz  19741  ringrz  19742  ringnegl  19748  rngnegr  19749  ringmneg1  19750  ringmneg2  19751  ringm2neg  19752  ringsubdi  19753  rngsubdir  19754  mulgass2  19755  ringlghm  19758  ringrghm  19759  gsumdixp  19763  prdsmulrcl  19765  imasring  19773  qusring2  19774  opprring  19788  dvdsrcl2  19807  dvdsrtr  19809  dvdsrmul1  19810  dvrcl  19843  dvrass  19847  irredrmul  19864  isdrngd  19931  subrgmcl  19951  abvtrivd  20015  srngmul  20033  issrngd  20036  idsrngd  20037  lmodmcl  20050  lmodprop2d  20100  rmodislmodlem  20105  prdslmodd  20146  sralmod  20370  2idlcpbl  20418  qusrhm  20421  quscrng  20424  frlmphl  20898  assa2ass  20980  assapropd  20986  ascldimul  21002  psrmulcllem  21066  psrvscacl  21072  psrlmod  21080  psrlidm  21082  psrridm  21083  psrass1  21084  psrdi  21085  psrdir  21086  psrass23l  21087  psrcom  21088  psrass23  21089  mplmonmul  21147  mplmon2mul  21187  mplind  21188  evlslem2  21199  evlslem3  21200  evlslem6  21201  evlslem1  21202  mpfind  21227  mhpmulcl  21249  psropprmul  21319  coe1mul2  21350  coe1tmmul2  21357  coe1tmmul  21358  evl1muld  21419  mamucl  21458  mamuass  21459  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  mamulid  21498  mamurid  21499  madetsmelbas  21521  madetsmelbas2  21522  mat1dimscm  21532  mat1dimmul  21533  mat1mhm  21541  dmatmul  21554  dmatmulcl  21557  scmatscmiddistr  21565  scmatscm  21570  scmatmulcl  21575  smatvscl  21581  scmatmhm  21591  mavmulcl  21604  mavmulass  21606  mdetleib2  21645  mdetf  21652  mdetrlin  21659  mdetrsca  21660  mdetrsca2  21661  mdetralt  21665  mdetero  21667  mdetuni0  21678  mdetmul  21680  m2detleib  21688  madugsum  21700  madulid  21702  cpmatmcllem  21775  cpmatmcl  21776  mat2pmatmul  21788  decpmatmullem  21828  decpmatmul  21829  decpmatmulsumfsupp  21830  pm2mpmhmlem1  21875  pm2mpmhmlem2  21876  chfacfisf  21911  chfacfscmulgsum  21917  chfacfpmmulcl  21918  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadugsumlemF  21933  cayhamlem4  21945  nrgdsdi  23735  nrgdsdir  23736  nrginvrcnlem  23761  mdegmullem  25148  coe1mul3  25169  deg1mul2  25184  deg1mul3  25185  deg1mul3le  25186  ply1domn  25193  ply1divmo  25205  ply1divex  25206  uc1pmon1p  25221  r1pcl  25227  r1pid  25229  dvdsq1p  25230  dvdsr1p  25231  ply1rem  25233  dchrelbas3  26291  dchrmulcl  26302  dchrinv  26314  abvcxp  26668  freshmansdream  31386  frobrhm  31387  rdivmuldivd  31390  ornglmulle  31406  orngrmulle  31407  ornglmullt  31408  orngrmullt  31409  orngmullt  31410  rhmpreimaidl  31505  elrspunidl  31508  rhmimaidl  31511  isprmidlc  31525  qsidomlem1  31530  qsidomlem2  31531  mxidlprm  31542  drgextlsp  31583  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  extdg1id  31640  mdetpmtr1  31675  matunitlindflem1  35700  matunitlindflem2  35701  lflnegcl  37016  lflvscl  37018  lkrlsp  37043  ldualvsass  37082  lclkrlem2m  39460  lclkrlem2o  39462  lclkrlem2p  39463  lcfrlem2  39484  lcfrlem3  39485  lcfrlem29  39512  mapdpglem30  39643  hdmapglem7  39870  isdomn4  40100  ringcld  40166  pwspjmhmmgpd  40192  evlsmulval  40201  mhphf  40208  prjspertr  40365  hbtlem2  40865  mendlmod  40934  mendassa  40935  isdomn3  40945  mon1psubm  40947  deg1mhm  40948  mnringmulrcld  41735  lidldomn1  45367  ply1mulgsum  45619  lincscm  45659  lincscmcl  45661  lincresunitlem2  45705  lmod1lem4  45719