Theorem ringcl 20323

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 2765	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20312	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20212	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 20211	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18790	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1179	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ‘cfv 6525  (class class class)co 7400  Basecbs 17259  ._rcmulr 17301  Mndcmnd 18782  mulGrpcmgp 20207  Ringcrg 20306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12225  df-2 12294  df-sets 17214  df-slot 17232  df-ndx 17244  df-base 17260  df-plusg 17313  df-mgm 18688  df-sgrp 18767  df-mnd 18783  df-mgp 20208  df-ring 20308

This theorem is referenced by:  ringcld  20333  ringnegl  20376  ringnegr  20377  ringmneg1  20378  ringmneg2  20379  mulgass2  20383  ringlghm  20386  ringrghm  20387  pwspjmhmmgpd  20400  imasring  20403  qusring2  20407  dvdsrcl2  20439  dvdsrtr  20441  dvdsrmul1  20442  dvrcl  20477  dvrass  20481  rdivmuldivd  20486  irredrmul  20500  isdomn3  20790  isdomn4  20791  drngmcl  20825  isdrngd  20838  isdrngdOLD  20840  abvtrivd  20904  srngmul  20924  issrngd  20927  idsrngd  20928  ornglmulle  20939  orngrmulle  20940  ornglmullt  20941  orngrmullt  20942  orngmullt  20943  lmodmcl  20963  lmodprop2d  21014  rmodislmodlem  21019  prdslmodd  21059  sralmod  21277  qusrhm  21377  rhmpreimaidl  21378  qusmul2idl  21380  isprmidlc  21434  qsidomlem1  21440  qsidomlem2  21441  freshmansdream  21684  frobrhm  21685  ascldimul  21998  psrvscacl  22061  psrlmod  22069  psrlidm  22071  psrridm  22072  psrdir  22075  psrcom  22077  mplmonmul  22147  mplmon2mul  22180  mplind  22181  evlslem2  22190  evlslem3  22191  evlslem6  22192  evlslem1  22193  mpfind  22226  evlsmulval  22241  psropprmul  22357  coe1mul2  22390  coe1tmmul2  22397  coe1tmmul  22398  evl1muld  22464  rhmply1vsca  22506  mamucl  22519  mamudi  22521  mamudir  22522  mamulid  22559  mamurid  22560  madetsmelbas  22582  madetsmelbas2  22583  mat1dimscm  22593  mat1dimmul  22594  mat1mhm  22602  dmatmul  22615  dmatmulcl  22618  scmatscmiddistr  22626  scmatscm  22631  scmatmulcl  22636  smatvscl  22642  scmatmhm  22652  mavmulcl  22665  mdetleib2  22706  mdetf  22713  mdetrlin  22720  mdetrsca2  22722  mdetralt  22726  mdetero  22728  mdetuni0  22739  mdetmul  22741  m2detleib  22749  madugsum  22761  madulid  22763  cpmatmcllem  22836  cpmatmcl  22837  mat2pmatmul  22849  decpmatmullem  22889  decpmatmul  22890  decpmatmulsumfsupp  22891  pm2mpmhmlem1  22936  pm2mpmhmlem2  22937  chfacfisf  22972  chfacfscmulgsum  22978  chfacfpmmulcl  22979  chfacfpmmulgsum  22982  chfacfpmmulgsum2  22983  cayhamlem1  22984  cpmadugsumlemF  22994  cayhamlem4  23006  nrgdsdi  24783  nrgdsdir  24784  nrginvrcnlem  24809  mdegmullem  26196  coe1mul3  26217  deg1mul2  26232  deg1mul3  26234  deg1mul3le  26235  ply1domn  26242  ply1divmo  26254  ply1divex  26255  uc1pmon1p  26270  r1pcl  26277  r1pid  26279  dvdsq1p  26281  dvdsr1p  26282  ply1rem  26284  dchrelbas3  27360  dchrmulcl  27371  dchrinv  27383  abvcxp  27737  elrspunidl  33652  rhmimaidl  33656  mxidlprm  33670  drgextlsp  33901  fedgmullem1  33936  fedgmullem2  33937  fedgmul  33938  extdg1id  33973  mdetpmtr1  34130  matunitlindflem1  38127  matunitlindflem2  38128  lflnegcl  39711  lflvscl  39713  lkrlsp  39738  ldualvsass  39777  lclkrlem2m  42155  lclkrlem2o  42157  lclkrlem2p  42158  lcfrlem2  42179  lcfrlem3  42180  lcfrlem29  42207  mapdpglem30  42338  hdmapglem7  42565  mhphf  43191  hbtlem2  43713  mendlmod  43778  mendassa  43779  mon1psubm  43788  deg1mhm  43789  mnringmulrcld  44816  lidldomn1  48851  ply1mulgsum  49021  lincscm  49061  lincscmcl  49063  lincresunitlem2  49107  lmod1lem4  49121