Theorem ringcl 20483

Description: Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised 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 2760	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20471	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20371	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 20370	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18937	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1181	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ‘cfv 6539  (class class class)co 7421  Basecbs 17393  ._rcmulr 17435  Mndcmnd 18929  mulGrpcmgp 20366  Ringcrg 20465

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-2 12409  df-sets 17348  df-slot 17366  df-ndx 17378  df-base 17394  df-plusg 17447  df-mgm 18822  df-sgrp 18914  df-mnd 18930  df-mgp 20367  df-ring 20467

This theorem is used by:  ringcld  20490  ringnegl  20539  ringnegr  20540  ringmneg1  20541  ringmneg2  20542  mulgass2  20546  ringlghm  20549  ringrghm  20550  pwspjmhmmgpd  20563  imasring  20566  qusring2  20570  dvdsrcl2  20602  dvdsrtr  20604  dvdsrmul1  20605  dvrcl  20640  dvrass  20644  rdivmuldivd  20649  irredrmul  20663  isdomn3  20972  isdomn4  20973  isdrng3lem2  21012  drngmcl  21015  isdrngd  21028  isdrngdOLD  21030  abvtrivd  21095  srngmul  21115  issrngd  21118  idsrngd  21119  ornglmulle  21130  orngrmulle  21131  ornglmullt  21132  orngrmullt  21133  orngmullt  21134  lmodmcl  21154  lmodprop2d  21205  rmodislmodlem  21210  prdslmodd  21250  sralmod  21468  qusrhm  21576  rhmpreimaidl  21577  qusmul2idl  21580  isprmidlc  21634  cmprmidlmcl  21637  qsidomlem1  21642  qsidomlem2  21643  freshmansdream  21886  frobrhm  21887  ascldimul  22202  psrvscacl  22265  psrlmod  22273  psrlidm  22275  psrridm  22276  psrdir  22279  psrcom  22281  mplmonmul  22351  mplmon2mul  22384  mplind  22385  evlslem2  22394  evlslem3  22395  evlslem6  22396  evlslem1  22397  mpfind  22430  evlsmulval  22445  psropprmul  22561  coe1mul2  22594  coe1tmmul2  22601  coe1tmmul  22602  evl1muld  22667  rhmply1vsca  22709  mamucl  22722  mamudi  22724  mamudir  22725  mamulid  22762  mamurid  22763  madetsmelbas  22785  madetsmelbas2  22786  mat1dimscm  22796  mat1dimmul  22797  mat1mhm  22805  dmatmul  22818  dmatmulcl  22821  scmatscmiddistr  22829  scmatscm  22834  scmatmulcl  22839  smatvscl  22845  scmatmhm  22855  mavmulcl  22868  mdetleib2  22909  mdetf  22916  mdetrlin  22923  mdetrsca2  22925  mdetralt  22929  mdetero  22931  mdetuni0  22942  mdetmul  22944  m2detleib  22952  madugsum  22964  madulid  22966  matunitlindflem1  23000  matunitlindflem2  23001  cpmatmcllem  23042  cpmatmcl  23043  mat2pmatmul  23055  decpmatmullem  23095  decpmatmul  23096  decpmatmulsumfsupp  23097  pm2mpmhmlem1  23142  pm2mpmhmlem2  23143  chfacfisf  23178  chfacfscmulgsum  23184  chfacfpmmulcl  23185  chfacfpmmulgsum  23188  chfacfpmmulgsum2  23189  cayhamlem1  23190  cpmadugsumlemF  23200  cayhamlem4  23212  nrgdsdi  24990  nrgdsdir  24991  nrginvrcnlem  25016  mdegmullem  26402  coe1mul3  26423  deg1mul2  26438  deg1mul3  26440  deg1mul3le  26441  ply1domn  26448  ply1divmo  26460  ply1divex  26461  uc1pmon1p  26476  r1pcl  26483  r1pid  26485  dvdsq1p  26487  dvdsr1p  26488  ply1rem  26490  dchrelbas3  27571  dchrmulcl  27582  dchrinv  27594  abvcxp  27948  rhmimaidl  34029  mxidlprm  34042  drgextlsp  34273  fedgmullem1  34308  fedgmullem2  34309  extdg1id  34345  mdetpmtr1  34502  lflnegcl  40226  lflvscl  40228  lkrlsp  40253  ldualvsass  40292  lclkrlem2m  42670  lclkrlem2o  42672  lclkrlem2p  42673  lcfrlem2  42694  lcfrlem3  42695  lcfrlem29  42722  mapdpglem30  42853  hdmapglem7  43080  mhphf  43719  hbtlem2  44220  mendlmod  44285  mendassa  44286  mon1psubm  44295  deg1mhm  44296  mnringmulrcld  45320  lidldomn1  49422  ply1mulgsum  49596  lincscm  49636  lincscmcl  49638  lincresunitlem2  49682  lmod1lem4  49696