Theorem ringcl 20159

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  ._rcmulr 17221  Mndcmnd 18661  mulGrpcmgp 20049  Ringcrg 20142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-2 12249  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-plusg 17233  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-mgp 20050  df-ring 20144

This theorem is referenced by:  ringcld  20169  ringnegl  20211  ringnegr  20212  ringmneg1  20213  ringmneg2  20214  mulgass2  20218  ringlghm  20221  ringrghm  20222  pwspjmhmmgpd  20237  imasring  20239  qusring2  20243  dvdsrcl2  20275  dvdsrtr  20277  dvdsrmul1  20278  dvrcl  20313  dvrass  20317  rdivmuldivd  20322  irredrmul  20336  isdomn3  20624  isdomn4  20625  drngmcl  20659  isdrngd  20674  isdrngdOLD  20676  abvtrivd  20741  srngmul  20761  issrngd  20764  idsrngd  20765  lmodmcl  20779  lmodprop2d  20830  rmodislmodlem  20835  prdslmodd  20875  sralmod  21094  qusrhm  21186  rhmpreimaidl  21187  qusmul2idl  21189  freshmansdream  21484  frobrhm  21485  ascldimul  21797  psrvscacl  21860  psrlmod  21869  psrlidm  21871  psrridm  21872  psrdir  21875  psrcom  21877  mplmonmul  21943  mplmon2mul  21976  mplind  21977  evlslem2  21986  evlslem3  21987  evlslem6  21988  evlslem1  21989  mpfind  22014  psropprmul  22122  coe1mul2  22155  coe1tmmul2  22162  coe1tmmul  22163  evl1muld  22230  rhmply1vsca  22275  mamucl  22288  mamudi  22290  mamudir  22291  mamulid  22328  mamurid  22329  madetsmelbas  22351  madetsmelbas2  22352  mat1dimscm  22362  mat1dimmul  22363  mat1mhm  22371  dmatmul  22384  dmatmulcl  22387  scmatscmiddistr  22395  scmatscm  22400  scmatmulcl  22405  smatvscl  22411  scmatmhm  22421  mavmulcl  22434  mdetleib2  22475  mdetf  22482  mdetrlin  22489  mdetrsca2  22491  mdetralt  22495  mdetero  22497  mdetuni0  22508  mdetmul  22510  m2detleib  22518  madugsum  22530  madulid  22532  cpmatmcllem  22605  cpmatmcl  22606  mat2pmatmul  22618  decpmatmullem  22658  decpmatmul  22659  decpmatmulsumfsupp  22660  pm2mpmhmlem1  22705  pm2mpmhmlem2  22706  chfacfisf  22741  chfacfscmulgsum  22747  chfacfpmmulcl  22748  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmadugsumlemF  22763  cayhamlem4  22775  nrgdsdi  24553  nrgdsdir  24554  nrginvrcnlem  24579  mdegmullem  25983  coe1mul3  26004  deg1mul2  26019  deg1mul3  26021  deg1mul3le  26022  ply1domn  26029  ply1divmo  26041  ply1divex  26042  uc1pmon1p  26057  r1pcl  26064  r1pid  26066  dvdsq1p  26068  dvdsr1p  26069  ply1rem  26071  dchrelbas3  27149  dchrmulcl  27160  dchrinv  27172  abvcxp  27526  ornglmulle  33283  orngrmulle  33284  ornglmullt  33285  orngrmullt  33286  orngmullt  33287  elrspunidl  33399  rhmimaidl  33403  isprmidlc  33418  qsidomlem1  33423  qsidomlem2  33424  mxidlprm  33441  drgextlsp  33589  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  extdg1id  33661  mdetpmtr1  33813  matunitlindflem1  37610  matunitlindflem2  37611  lflnegcl  39068  lflvscl  39070  lkrlsp  39095  ldualvsass  39134  lclkrlem2m  41513  lclkrlem2o  41515  lclkrlem2p  41516  lcfrlem2  41537  lcfrlem3  41538  lcfrlem29  41565  mapdpglem30  41696  hdmapglem7  41923  evlsmulval  42557  mhphf  42585  hbtlem2  43113  mendlmod  43178  mendassa  43179  mon1psubm  43188  deg1mhm  43189  mnringmulrcld  44217  lidldomn1  48219  ply1mulgsum  48379  lincscm  48419  lincscmcl  48421  lincresunitlem2  48465  lmod1lem4  48479