Theorem ringcl 20231

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  ._rcmulr 17221  Mndcmnd 18702  mulGrpcmgp 20121  Ringcrg 20214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-2 12244  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-plusg 17233  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-mgp 20122  df-ring 20216

This theorem is referenced by:  ringcld  20241  ringnegl  20283  ringnegr  20284  ringmneg1  20285  ringmneg2  20286  mulgass2  20290  ringlghm  20293  ringrghm  20294  pwspjmhmmgpd  20307  imasring  20310  qusring2  20314  dvdsrcl2  20346  dvdsrtr  20348  dvdsrmul1  20349  dvrcl  20384  dvrass  20388  rdivmuldivd  20393  irredrmul  20407  isdomn3  20692  isdomn4  20693  drngmcl  20727  isdrngd  20742  isdrngdOLD  20744  abvtrivd  20809  srngmul  20829  issrngd  20832  idsrngd  20833  ornglmulle  20844  orngrmulle  20845  ornglmullt  20846  orngrmullt  20847  orngmullt  20848  lmodmcl  20868  lmodprop2d  20919  rmodislmodlem  20924  prdslmodd  20964  sralmod  21182  qusrhm  21274  rhmpreimaidl  21275  qusmul2idl  21277  freshmansdream  21554  frobrhm  21555  ascldimul  21868  psrvscacl  21930  psrlmod  21938  psrlidm  21940  psrridm  21941  psrdir  21944  psrcom  21946  mplmonmul  22014  mplmon2mul  22047  mplind  22048  evlslem2  22057  evlslem3  22058  evlslem6  22059  evlslem1  22060  mpfind  22093  psropprmul  22201  coe1mul2  22234  coe1tmmul2  22241  coe1tmmul  22242  evl1muld  22308  rhmply1vsca  22353  mamucl  22366  mamudi  22368  mamudir  22369  mamulid  22406  mamurid  22407  madetsmelbas  22429  madetsmelbas2  22430  mat1dimscm  22440  mat1dimmul  22441  mat1mhm  22449  dmatmul  22462  dmatmulcl  22465  scmatscmiddistr  22473  scmatscm  22478  scmatmulcl  22483  smatvscl  22489  scmatmhm  22499  mavmulcl  22512  mdetleib2  22553  mdetf  22560  mdetrlin  22567  mdetrsca2  22569  mdetralt  22573  mdetero  22575  mdetuni0  22586  mdetmul  22588  m2detleib  22596  madugsum  22608  madulid  22610  cpmatmcllem  22683  cpmatmcl  22684  mat2pmatmul  22696  decpmatmullem  22736  decpmatmul  22737  decpmatmulsumfsupp  22738  pm2mpmhmlem1  22783  pm2mpmhmlem2  22784  chfacfisf  22819  chfacfscmulgsum  22825  chfacfpmmulcl  22826  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadugsumlemF  22841  cayhamlem4  22853  nrgdsdi  24630  nrgdsdir  24631  nrginvrcnlem  24656  mdegmullem  26043  coe1mul3  26064  deg1mul2  26079  deg1mul3  26081  deg1mul3le  26082  ply1domn  26089  ply1divmo  26101  ply1divex  26102  uc1pmon1p  26117  r1pcl  26124  r1pid  26126  dvdsq1p  26128  dvdsr1p  26129  ply1rem  26131  dchrelbas3  27201  dchrmulcl  27212  dchrinv  27224  abvcxp  27578  elrspunidl  33488  rhmimaidl  33492  isprmidlc  33507  qsidomlem1  33512  qsidomlem2  33513  mxidlprm  33530  drgextlsp  33738  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  extdg1id  33810  mdetpmtr1  33967  matunitlindflem1  37937  matunitlindflem2  37938  lflnegcl  39521  lflvscl  39523  lkrlsp  39548  ldualvsass  39587  lclkrlem2m  41965  lclkrlem2o  41967  lclkrlem2p  41968  lcfrlem2  41989  lcfrlem3  41990  lcfrlem29  42017  mapdpglem30  42148  hdmapglem7  42375  evlsmulval  43005  mhphf  43030  hbtlem2  43552  mendlmod  43617  mendassa  43618  mon1psubm  43627  deg1mhm  43628  mnringmulrcld  44655  lidldomn1  48707  ply1mulgsum  48866  lincscm  48906  lincscmcl  48908  lincresunitlem2  48952  lmod1lem4  48966