Theorem ringcl 20457

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 2761	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	ringmgp 20445	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 20345	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 20344	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18911	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1181	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6531  (class class class)co 7412  Basecbs 17367  ._rcmulr 17409  Mndcmnd 18903  mulGrpcmgp 20340  Ringcrg 20439

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-nn 12317  df-2 12386  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-plusg 17421  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-mgp 20341  df-ring 20441

This theorem is used by:  ringcld  20464  ringnegl  20513  ringnegr  20514  ringmneg1  20515  ringmneg2  20516  mulgass2  20520  ringlghm  20523  ringrghm  20524  pwspjmhmmgpd  20537  imasring  20540  qusring2  20544  dvdsrcl2  20576  dvdsrtr  20578  dvdsrmul1  20579  dvrcl  20614  dvrass  20618  rdivmuldivd  20623  irredrmul  20637  isdomn3  20946  isdomn4  20947  isdrng3lem2  20986  drngmcl  20989  isdrngd  21002  isdrngdOLD  21004  abvtrivd  21069  srngmul  21089  issrngd  21092  idsrngd  21093  ornglmulle  21104  orngrmulle  21105  ornglmullt  21106  orngrmullt  21107  orngmullt  21108  lmodmcl  21128  lmodprop2d  21179  rmodislmodlem  21184  prdslmodd  21224  sralmod  21442  qusrhm  21550  rhmpreimaidl  21551  qusmul2idl  21554  isprmidlc  21608  cmprmidlmcl  21611  qsidomlem1  21616  qsidomlem2  21617  freshmansdream  21860  frobrhm  21861  ascldimul  22176  psrvscacl  22239  psrlmod  22247  psrlidm  22249  psrridm  22250  psrdir  22253  psrcom  22255  mplmonmul  22325  mplmon2mul  22358  mplind  22359  evlslem2  22368  evlslem3  22369  evlslem6  22370  evlslem1  22371  mpfind  22404  evlsmulval  22419  psropprmul  22535  coe1mul2  22568  coe1tmmul2  22575  coe1tmmul  22576  evl1muld  22641  rhmply1vsca  22683  mamucl  22696  mamudi  22698  mamudir  22699  mamulid  22736  mamurid  22737  madetsmelbas  22759  madetsmelbas2  22760  mat1dimscm  22770  mat1dimmul  22771  mat1mhm  22779  dmatmul  22792  dmatmulcl  22795  scmatscmiddistr  22803  scmatscm  22808  scmatmulcl  22813  smatvscl  22819  scmatmhm  22829  mavmulcl  22842  mdetleib2  22883  mdetf  22890  mdetrlin  22897  mdetrsca2  22899  mdetralt  22903  mdetero  22905  mdetuni0  22916  mdetmul  22918  m2detleib  22926  madugsum  22938  madulid  22940  matunitlindflem1  22974  matunitlindflem2  22975  cpmatmcllem  23016  cpmatmcl  23017  mat2pmatmul  23029  decpmatmullem  23069  decpmatmul  23070  decpmatmulsumfsupp  23071  pm2mpmhmlem1  23116  pm2mpmhmlem2  23117  chfacfisf  23152  chfacfscmulgsum  23158  chfacfpmmulcl  23159  chfacfpmmulgsum  23162  chfacfpmmulgsum2  23163  cayhamlem1  23164  cpmadugsumlemF  23174  cayhamlem4  23186  nrgdsdi  24964  nrgdsdir  24965  nrginvrcnlem  24990  mdegmullem  26376  coe1mul3  26397  deg1mul2  26412  deg1mul3  26414  deg1mul3le  26415  ply1domn  26422  ply1divmo  26434  ply1divex  26435  uc1pmon1p  26450  r1pcl  26457  r1pid  26459  dvdsq1p  26461  dvdsr1p  26462  ply1rem  26464  dchrelbas3  27547  dchrmulcl  27558  dchrinv  27570  abvcxp  27924  elrspunidl  33960  rhmimaidl  33964  mxidlprm  33977  drgextlsp  34208  fedgmullem1  34243  fedgmullem2  34244  fedgmul  34245  extdg1id  34280  mdetpmtr1  34437  lflnegcl  40100  lflvscl  40102  lkrlsp  40127  ldualvsass  40166  lclkrlem2m  42544  lclkrlem2o  42546  lclkrlem2p  42547  lcfrlem2  42568  lcfrlem3  42569  lcfrlem29  42596  mapdpglem30  42727  hdmapglem7  42954  mhphf  43587  hbtlem2  44084  mendlmod  44149  mendassa  44150  mon1psubm  44159  deg1mhm  44160  mnringmulrcld  45185  lidldomn1  49272  ply1mulgsum  49446  lincscm  49486  lincscmcl  49488  lincresunitlem2  49532  lmod1lem4  49546