Theorem ringcl 20067

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 2733	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20056	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 19988	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 19986	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18630	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1164	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ‘cfv 6541  (class class class)co 7406  Basecbs 17141  ._rcmulr 17195  Mndcmnd 18622  mulGrpcmgp 19982  Ringcrg 20050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-2 12272  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-plusg 17207  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-mgp 19983  df-ring 20052

This theorem is referenced by:  ringcld  20074  ringlz  20101  ringrz  20102  ringnegl  20108  ringnegr  20109  ringmneg1  20110  ringmneg2  20111  ringm2neg  20112  ringsubdi  20113  ringsubdir  20114  mulgass2  20115  ringlghm  20118  ringrghm  20119  prdsmulrcl  20127  pwspjmhmmgpd  20135  imasring  20137  qusring2  20140  opprring  20154  dvdsrcl2  20173  dvdsrtr  20175  dvdsrmul1  20176  dvrcl  20211  dvrass  20215  rdivmuldivd  20220  irredrmul  20234  isdrngd  20341  isdrngdOLD  20343  subrgmcl  20368  abvtrivd  20441  srngmul  20459  issrngd  20462  idsrngd  20463  lmodmcl  20477  lmodprop2d  20527  rmodislmodlem  20532  prdslmodd  20573  sralmod  20802  qusrhm  20867  qusmul2  20868  quscrng  20871  isdomn4  20911  assa2ass  21410  ascldimul  21434  psrvscacl  21504  psrlmod  21513  psrlidm  21515  psrridm  21516  psrdi  21518  psrdir  21519  psrcom  21521  mplmonmul  21583  mplmon2mul  21622  mplind  21623  evlslem2  21634  evlslem3  21635  evlslem6  21636  evlslem1  21637  mpfind  21662  mhpmulcl  21684  psropprmul  21752  coe1mul2  21783  coe1tmmul2  21790  coe1tmmul  21791  evl1muld  21854  mamucl  21893  mamudi  21895  mamudir  21896  mamulid  21935  mamurid  21936  madetsmelbas  21958  madetsmelbas2  21959  mat1dimscm  21969  mat1dimmul  21970  mat1mhm  21978  dmatmul  21991  dmatmulcl  21994  scmatscmiddistr  22002  scmatscm  22007  scmatmulcl  22012  smatvscl  22018  scmatmhm  22028  mavmulcl  22041  mdetleib2  22082  mdetf  22089  mdetrlin  22096  mdetrsca2  22098  mdetralt  22102  mdetero  22104  mdetuni0  22115  mdetmul  22117  m2detleib  22125  madugsum  22137  madulid  22139  cpmatmcllem  22212  cpmatmcl  22213  mat2pmatmul  22225  decpmatmullem  22265  decpmatmul  22266  decpmatmulsumfsupp  22267  pm2mpmhmlem1  22312  pm2mpmhmlem2  22313  chfacfisf  22348  chfacfscmulgsum  22354  chfacfpmmulcl  22355  chfacfpmmulgsum  22358  chfacfpmmulgsum2  22359  cayhamlem1  22360  cpmadugsumlemF  22370  cayhamlem4  22382  nrgdsdi  24174  nrgdsdir  24175  nrginvrcnlem  24200  mdegmullem  25588  coe1mul3  25609  deg1mul2  25624  deg1mul3  25625  deg1mul3le  25626  ply1domn  25633  ply1divmo  25645  ply1divex  25646  uc1pmon1p  25661  r1pcl  25667  r1pid  25669  dvdsq1p  25670  dvdsr1p  25671  ply1rem  25673  dchrelbas3  26731  dchrmulcl  26742  dchrinv  26754  abvcxp  27108  freshmansdream  32370  frobrhm  32371  ornglmulle  32412  orngrmulle  32413  ornglmullt  32414  orngrmullt  32415  orngmullt  32416  qusmul  32504  rhmpreimaidl  32526  elrspunidl  32535  rhmimaidl  32539  isprmidlc  32555  qsidomlem1  32560  qsidomlem2  32561  mxidlprm  32575  drgextlsp  32670  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  extdg1id  32731  mdetpmtr1  32792  matunitlindflem1  36473  matunitlindflem2  36474  lflnegcl  37934  lflvscl  37936  lkrlsp  37961  ldualvsass  38000  lclkrlem2m  40379  lclkrlem2o  40381  lclkrlem2p  40382  lcfrlem2  40403  lcfrlem3  40404  lcfrlem29  40431  mapdpglem30  40562  hdmapglem7  40789  evlsmulval  41139  mhphf  41167  prjspertr  41344  hbtlem2  41852  mendlmod  41921  mendassa  41922  isdomn3  41932  mon1psubm  41934  deg1mhm  41935  mnringmulrcld  42973  lidldomn1  46777  ply1mulgsum  47025  lincscm  47065  lincscmcl  47067  lincresunitlem2  47111  lmod1lem4  47125