Theorem ringcl 20169

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 2731	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20158	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20064	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 20063	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18650	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1163	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  ._rcmulr 17162  Mndcmnd 18642  mulGrpcmgp 20059  Ringcrg 20152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-nn 12126  df-2 12188  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-plusg 17174  df-mgm 18548  df-sgrp 18627  df-mnd 18643  df-mgp 20060  df-ring 20154

This theorem is referenced by:  ringcld  20179  ringnegl  20221  ringnegr  20222  ringmneg1  20223  ringmneg2  20224  mulgass2  20228  ringlghm  20231  ringrghm  20232  pwspjmhmmgpd  20247  imasring  20249  qusring2  20253  dvdsrcl2  20285  dvdsrtr  20287  dvdsrmul1  20288  dvrcl  20323  dvrass  20327  rdivmuldivd  20332  irredrmul  20346  isdomn3  20631  isdomn4  20632  drngmcl  20666  isdrngd  20681  isdrngdOLD  20683  abvtrivd  20748  srngmul  20768  issrngd  20771  idsrngd  20772  ornglmulle  20783  orngrmulle  20784  ornglmullt  20785  orngrmullt  20786  orngmullt  20787  lmodmcl  20807  lmodprop2d  20858  rmodislmodlem  20863  prdslmodd  20903  sralmod  21122  qusrhm  21214  rhmpreimaidl  21215  qusmul2idl  21217  freshmansdream  21512  frobrhm  21513  ascldimul  21826  psrvscacl  21889  psrlmod  21898  psrlidm  21900  psrridm  21901  psrdir  21904  psrcom  21906  mplmonmul  21972  mplmon2mul  22005  mplind  22006  evlslem2  22015  evlslem3  22016  evlslem6  22017  evlslem1  22018  mpfind  22043  psropprmul  22151  coe1mul2  22184  coe1tmmul2  22191  coe1tmmul  22192  evl1muld  22259  rhmply1vsca  22304  mamucl  22317  mamudi  22319  mamudir  22320  mamulid  22357  mamurid  22358  madetsmelbas  22380  madetsmelbas2  22381  mat1dimscm  22391  mat1dimmul  22392  mat1mhm  22400  dmatmul  22413  dmatmulcl  22416  scmatscmiddistr  22424  scmatscm  22429  scmatmulcl  22434  smatvscl  22440  scmatmhm  22450  mavmulcl  22463  mdetleib2  22504  mdetf  22511  mdetrlin  22518  mdetrsca2  22520  mdetralt  22524  mdetero  22526  mdetuni0  22537  mdetmul  22539  m2detleib  22547  madugsum  22559  madulid  22561  cpmatmcllem  22634  cpmatmcl  22635  mat2pmatmul  22647  decpmatmullem  22687  decpmatmul  22688  decpmatmulsumfsupp  22689  pm2mpmhmlem1  22734  pm2mpmhmlem2  22735  chfacfisf  22770  chfacfscmulgsum  22776  chfacfpmmulcl  22777  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmadugsumlemF  22792  cayhamlem4  22804  nrgdsdi  24581  nrgdsdir  24582  nrginvrcnlem  24607  mdegmullem  26011  coe1mul3  26032  deg1mul2  26047  deg1mul3  26049  deg1mul3le  26050  ply1domn  26057  ply1divmo  26069  ply1divex  26070  uc1pmon1p  26085  r1pcl  26092  r1pid  26094  dvdsq1p  26096  dvdsr1p  26097  ply1rem  26099  dchrelbas3  27177  dchrmulcl  27188  dchrinv  27200  abvcxp  27554  elrspunidl  33391  rhmimaidl  33395  isprmidlc  33410  qsidomlem1  33415  qsidomlem2  33416  mxidlprm  33433  drgextlsp  33604  fedgmullem1  33640  fedgmullem2  33641  fedgmul  33642  extdg1id  33677  mdetpmtr1  33834  matunitlindflem1  37662  matunitlindflem2  37663  lflnegcl  39120  lflvscl  39122  lkrlsp  39147  ldualvsass  39186  lclkrlem2m  41564  lclkrlem2o  41566  lclkrlem2p  41567  lcfrlem2  41588  lcfrlem3  41589  lcfrlem29  41616  mapdpglem30  41747  hdmapglem7  41974  evlsmulval  42608  mhphf  42636  hbtlem2  43163  mendlmod  43228  mendassa  43229  mon1psubm  43238  deg1mhm  43239  mnringmulrcld  44267  lidldomn1  48268  ply1mulgsum  48428  lincscm  48468  lincscmcl  48470  lincresunitlem2  48514  lmod1lem4  48528