Theorem ringcl 20222

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  ._rcmulr 17212  Mndcmnd 18693  mulGrpcmgp 20112  Ringcrg 20205

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 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-plusg 17224  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mgp 20113  df-ring 20207

This theorem is referenced by:  ringcld  20232  ringnegl  20274  ringnegr  20275  ringmneg1  20276  ringmneg2  20277  mulgass2  20281  ringlghm  20284  ringrghm  20285  pwspjmhmmgpd  20298  imasring  20301  qusring2  20305  dvdsrcl2  20337  dvdsrtr  20339  dvdsrmul1  20340  dvrcl  20375  dvrass  20379  rdivmuldivd  20384  irredrmul  20398  isdomn3  20683  isdomn4  20684  drngmcl  20718  isdrngd  20733  isdrngdOLD  20735  abvtrivd  20800  srngmul  20820  issrngd  20823  idsrngd  20824  ornglmulle  20835  orngrmulle  20836  ornglmullt  20837  orngrmullt  20838  orngmullt  20839  lmodmcl  20859  lmodprop2d  20910  rmodislmodlem  20915  prdslmodd  20955  sralmod  21174  qusrhm  21266  rhmpreimaidl  21267  qusmul2idl  21269  freshmansdream  21564  frobrhm  21565  ascldimul  21878  psrvscacl  21940  psrlmod  21948  psrlidm  21950  psrridm  21951  psrdir  21954  psrcom  21956  mplmonmul  22024  mplmon2mul  22057  mplind  22058  evlslem2  22067  evlslem3  22068  evlslem6  22069  evlslem1  22070  mpfind  22103  psropprmul  22211  coe1mul2  22244  coe1tmmul2  22251  coe1tmmul  22252  evl1muld  22318  rhmply1vsca  22363  mamucl  22376  mamudi  22378  mamudir  22379  mamulid  22416  mamurid  22417  madetsmelbas  22439  madetsmelbas2  22440  mat1dimscm  22450  mat1dimmul  22451  mat1mhm  22459  dmatmul  22472  dmatmulcl  22475  scmatscmiddistr  22483  scmatscm  22488  scmatmulcl  22493  smatvscl  22499  scmatmhm  22509  mavmulcl  22522  mdetleib2  22563  mdetf  22570  mdetrlin  22577  mdetrsca2  22579  mdetralt  22583  mdetero  22585  mdetuni0  22596  mdetmul  22598  m2detleib  22606  madugsum  22618  madulid  22620  cpmatmcllem  22693  cpmatmcl  22694  mat2pmatmul  22706  decpmatmullem  22746  decpmatmul  22747  decpmatmulsumfsupp  22748  pm2mpmhmlem1  22793  pm2mpmhmlem2  22794  chfacfisf  22829  chfacfscmulgsum  22835  chfacfpmmulcl  22836  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmadugsumlemF  22851  cayhamlem4  22863  nrgdsdi  24640  nrgdsdir  24641  nrginvrcnlem  24666  mdegmullem  26053  coe1mul3  26074  deg1mul2  26089  deg1mul3  26091  deg1mul3le  26092  ply1domn  26099  ply1divmo  26111  ply1divex  26112  uc1pmon1p  26127  r1pcl  26134  r1pid  26136  dvdsq1p  26138  dvdsr1p  26139  ply1rem  26141  dchrelbas3  27215  dchrmulcl  27226  dchrinv  27238  abvcxp  27592  elrspunidl  33503  rhmimaidl  33507  isprmidlc  33522  qsidomlem1  33527  qsidomlem2  33528  mxidlprm  33545  drgextlsp  33753  fedgmullem1  33789  fedgmullem2  33790  fedgmul  33791  extdg1id  33826  mdetpmtr1  33983  matunitlindflem1  37951  matunitlindflem2  37952  lflnegcl  39535  lflvscl  39537  lkrlsp  39562  ldualvsass  39601  lclkrlem2m  41979  lclkrlem2o  41981  lclkrlem2p  41982  lcfrlem2  42003  lcfrlem3  42004  lcfrlem29  42031  mapdpglem30  42162  hdmapglem7  42389  evlsmulval  43019  mhphf  43044  hbtlem2  43570  mendlmod  43635  mendassa  43636  mon1psubm  43645  deg1mhm  43646  mnringmulrcld  44673  lidldomn1  48719  ply1mulgsum  48878  lincscm  48918  lincscmcl  48920  lincresunitlem2  48964  lmod1lem4  48978