Theorem ringcl 19868

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 19857	. 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
3		ringcl.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	1, 3	mgpbas 19794	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
5		ringcl.t	. . . 4 ⊢ · = (.r‘𝑅)
6	1, 5	mgpplusg 19792	. . 3 ⊢ · = (+g‘(mulGrp‘𝑅))
7	4, 6	mndcl 18463	. 2 ⊢ (((mulGrp‘𝑅) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
8	2, 7	syl3an1 1162	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ‘cfv 6465  (class class class)co 7315  Basecbs 16982  ._rcmulr 17033  Mndcmnd 18455  mulGrpcmgp 19788  Ringcrg 19851

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-nn 12047  df-2 12109  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-plusg 17045  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-mgp 19789  df-ring 19853

This theorem is referenced by:  ringlz  19894  ringrz  19895  ringnegl  19901  rngnegr  19902  ringmneg1  19903  ringmneg2  19904  ringm2neg  19905  ringsubdi  19906  rngsubdir  19907  mulgass2  19908  ringlghm  19911  ringrghm  19912  gsumdixp  19916  prdsmulrcl  19918  imasring  19926  qusring2  19927  opprring  19941  dvdsrcl2  19960  dvdsrtr  19962  dvdsrmul1  19963  dvrcl  19996  dvrass  20000  irredrmul  20017  isdrngd  20088  subrgmcl  20108  abvtrivd  20172  srngmul  20190  issrngd  20193  idsrngd  20194  lmodmcl  20207  lmodprop2d  20257  rmodislmodlem  20262  prdslmodd  20303  sralmod  20529  2idlcpbl  20577  qusrhm  20580  quscrng  20583  frlmphl  21060  assa2ass  21142  assapropd  21148  ascldimul  21164  psrmulcllem  21228  psrvscacl  21234  psrlmod  21242  psrlidm  21244  psrridm  21245  psrass1  21246  psrdi  21247  psrdir  21248  psrass23l  21249  psrcom  21250  psrass23  21251  mplmonmul  21309  mplmon2mul  21349  mplind  21350  evlslem2  21361  evlslem3  21362  evlslem6  21363  evlslem1  21364  mpfind  21389  mhpmulcl  21411  psropprmul  21481  coe1mul2  21512  coe1tmmul2  21519  coe1tmmul  21520  evl1muld  21581  mamucl  21620  mamuass  21621  mamudi  21622  mamudir  21623  mamuvs1  21624  mamuvs2  21625  mamulid  21662  mamurid  21663  madetsmelbas  21685  madetsmelbas2  21686  mat1dimscm  21696  mat1dimmul  21697  mat1mhm  21705  dmatmul  21718  dmatmulcl  21721  scmatscmiddistr  21729  scmatscm  21734  scmatmulcl  21739  smatvscl  21745  scmatmhm  21755  mavmulcl  21768  mavmulass  21770  mdetleib2  21809  mdetf  21816  mdetrlin  21823  mdetrsca  21824  mdetrsca2  21825  mdetralt  21829  mdetero  21831  mdetuni0  21842  mdetmul  21844  m2detleib  21852  madugsum  21864  madulid  21866  cpmatmcllem  21939  cpmatmcl  21940  mat2pmatmul  21952  decpmatmullem  21992  decpmatmul  21993  decpmatmulsumfsupp  21994  pm2mpmhmlem1  22039  pm2mpmhmlem2  22040  chfacfisf  22075  chfacfscmulgsum  22081  chfacfpmmulcl  22082  chfacfpmmulgsum  22085  chfacfpmmulgsum2  22086  cayhamlem1  22087  cpmadugsumlemF  22097  cayhamlem4  22109  nrgdsdi  23901  nrgdsdir  23902  nrginvrcnlem  23927  mdegmullem  25315  coe1mul3  25336  deg1mul2  25351  deg1mul3  25352  deg1mul3le  25353  ply1domn  25360  ply1divmo  25372  ply1divex  25373  uc1pmon1p  25388  r1pcl  25394  r1pid  25396  dvdsq1p  25397  dvdsr1p  25398  ply1rem  25400  dchrelbas3  26458  dchrmulcl  26469  dchrinv  26481  abvcxp  26835  freshmansdream  31592  frobrhm  31593  rdivmuldivd  31596  ornglmulle  31612  orngrmulle  31613  ornglmullt  31614  orngrmullt  31615  orngmullt  31616  rhmpreimaidl  31708  elrspunidl  31711  rhmimaidl  31714  isprmidlc  31728  qsidomlem1  31733  qsidomlem2  31734  mxidlprm  31745  drgextlsp  31787  fedgmullem1  31816  fedgmullem2  31817  fedgmul  31818  extdg1id  31844  mdetpmtr1  31879  matunitlindflem1  35829  matunitlindflem2  35830  lflnegcl  37293  lflvscl  37295  lkrlsp  37320  ldualvsass  37359  lclkrlem2m  39738  lclkrlem2o  39740  lclkrlem2p  39741  lcfrlem2  39762  lcfrlem3  39763  lcfrlem29  39790  mapdpglem30  39921  hdmapglem7  40148  isdomn4  40380  ringcld  40443  pwspjmhmmgpd  40470  evlsmulval  40481  mhphf  40488  prjspertr  40647  hbtlem2  41153  mendlmod  41222  mendassa  41223  isdomn3  41233  mon1psubm  41235  deg1mhm  41236  mnringmulrcld  42067  lidldomn1  45731  ply1mulgsum  45983  lincscm  46023  lincscmcl  46025  lincresunitlem2  46069  lmod1lem4  46083