Theorem ringcl 20333

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 2763	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20322	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20222	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 20221	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18801	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1181	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  ._rcmulr 17312  Mndcmnd 18793  mulGrpcmgp 20217  Ringcrg 20316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-2 12304  df-sets 17225  df-slot 17243  df-ndx 17255  df-base 17271  df-plusg 17324  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-mgp 20218  df-ring 20318

This theorem is referenced by:  ringcld  20343  ringnegl  20386  ringnegr  20387  ringmneg1  20388  ringmneg2  20389  mulgass2  20393  ringlghm  20396  ringrghm  20397  pwspjmhmmgpd  20410  imasring  20413  qusring2  20417  dvdsrcl2  20449  dvdsrtr  20451  dvdsrmul1  20452  dvrcl  20487  dvrass  20491  rdivmuldivd  20496  irredrmul  20510  isdomn3  20800  isdomn4  20801  drngmcl  20837  isdrngd  20850  isdrngdOLD  20852  abvtrivd  20916  srngmul  20936  issrngd  20939  idsrngd  20940  ornglmulle  20951  orngrmulle  20952  ornglmullt  20953  orngrmullt  20954  orngmullt  20955  lmodmcl  20975  lmodprop2d  21026  rmodislmodlem  21031  prdslmodd  21071  sralmod  21289  qusrhm  21396  rhmpreimaidl  21397  qusmul2idl  21399  isprmidlc  21453  cmprmidlmcl  21456  qsidomlem1  21461  qsidomlem2  21462  freshmansdream  21705  frobrhm  21706  ascldimul  22019  psrvscacl  22082  psrlmod  22090  psrlidm  22092  psrridm  22093  psrdir  22096  psrcom  22098  mplmonmul  22168  mplmon2mul  22201  mplind  22202  evlslem2  22211  evlslem3  22212  evlslem6  22213  evlslem1  22214  mpfind  22247  evlsmulval  22262  psropprmul  22378  coe1mul2  22411  coe1tmmul2  22418  coe1tmmul  22419  evl1muld  22484  rhmply1vsca  22526  mamucl  22539  mamudi  22541  mamudir  22542  mamulid  22579  mamurid  22580  madetsmelbas  22602  madetsmelbas2  22603  mat1dimscm  22613  mat1dimmul  22614  mat1mhm  22622  dmatmul  22635  dmatmulcl  22638  scmatscmiddistr  22646  scmatscm  22651  scmatmulcl  22656  smatvscl  22662  scmatmhm  22672  mavmulcl  22685  mdetleib2  22726  mdetf  22733  mdetrlin  22740  mdetrsca2  22742  mdetralt  22746  mdetero  22748  mdetuni0  22759  mdetmul  22761  m2detleib  22769  madugsum  22781  madulid  22783  cpmatmcllem  22856  cpmatmcl  22857  mat2pmatmul  22869  decpmatmullem  22909  decpmatmul  22910  decpmatmulsumfsupp  22911  pm2mpmhmlem1  22956  pm2mpmhmlem2  22957  chfacfisf  22992  chfacfscmulgsum  22998  chfacfpmmulcl  22999  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmadugsumlemF  23014  cayhamlem4  23026  nrgdsdi  24803  nrgdsdir  24804  nrginvrcnlem  24829  mdegmullem  26216  coe1mul3  26237  deg1mul2  26252  deg1mul3  26254  deg1mul3le  26255  ply1domn  26262  ply1divmo  26274  ply1divex  26275  uc1pmon1p  26290  r1pcl  26297  r1pid  26299  dvdsq1p  26301  dvdsr1p  26302  ply1rem  26304  dchrelbas3  27383  dchrmulcl  27394  dchrinv  27406  abvcxp  27760  elrspunidl  33717  rhmimaidl  33721  mxidlprm  33734  drgextlsp  33965  fedgmullem1  34000  fedgmullem2  34001  fedgmul  34002  extdg1id  34037  mdetpmtr1  34194  matunitlindflem1  38248  matunitlindflem2  38249  lflnegcl  39830  lflvscl  39832  lkrlsp  39857  ldualvsass  39896  lclkrlem2m  42274  lclkrlem2o  42276  lclkrlem2p  42277  lcfrlem2  42298  lcfrlem3  42299  lcfrlem29  42326  mapdpglem30  42457  hdmapglem7  42684  mhphf  43312  hbtlem2  43834  mendlmod  43899  mendassa  43900  mon1psubm  43909  deg1mhm  43910  mnringmulrcld  44935  lidldomn1  48979  ply1mulgsum  49153  lincscm  49193  lincscmcl  49195  lincresunitlem2  49239  lmod1lem4  49253