Theorem ringcl 20215

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  ._rcmulr 17277  Mndcmnd 18717  mulGrpcmgp 20105  Ringcrg 20198

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 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-2 12308  df-sets 17188  df-slot 17206  df-ndx 17218  df-base 17234  df-plusg 17289  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-mgp 20106  df-ring 20200

This theorem is referenced by:  ringcld  20225  ringnegl  20267  ringnegr  20268  ringmneg1  20269  ringmneg2  20270  mulgass2  20274  ringlghm  20277  ringrghm  20278  pwspjmhmmgpd  20293  imasring  20295  qusring2  20299  dvdsrcl2  20331  dvdsrtr  20333  dvdsrmul1  20334  dvrcl  20369  dvrass  20373  rdivmuldivd  20378  irredrmul  20392  isdomn3  20680  isdomn4  20681  drngmcl  20715  isdrngd  20730  isdrngdOLD  20732  abvtrivd  20797  srngmul  20817  issrngd  20820  idsrngd  20821  lmodmcl  20835  lmodprop2d  20886  rmodislmodlem  20891  prdslmodd  20931  sralmod  21150  qusrhm  21242  rhmpreimaidl  21243  qusmul2idl  21245  freshmansdream  21540  frobrhm  21541  ascldimul  21853  psrvscacl  21916  psrlmod  21925  psrlidm  21927  psrridm  21928  psrdir  21931  psrcom  21933  mplmonmul  21999  mplmon2mul  22032  mplind  22033  evlslem2  22042  evlslem3  22043  evlslem6  22044  evlslem1  22045  mpfind  22070  psropprmul  22178  coe1mul2  22211  coe1tmmul2  22218  coe1tmmul  22219  evl1muld  22286  rhmply1vsca  22331  mamucl  22344  mamudi  22346  mamudir  22347  mamulid  22384  mamurid  22385  madetsmelbas  22407  madetsmelbas2  22408  mat1dimscm  22418  mat1dimmul  22419  mat1mhm  22427  dmatmul  22440  dmatmulcl  22443  scmatscmiddistr  22451  scmatscm  22456  scmatmulcl  22461  smatvscl  22467  scmatmhm  22477  mavmulcl  22490  mdetleib2  22531  mdetf  22538  mdetrlin  22545  mdetrsca2  22547  mdetralt  22551  mdetero  22553  mdetuni0  22564  mdetmul  22566  m2detleib  22574  madugsum  22586  madulid  22588  cpmatmcllem  22661  cpmatmcl  22662  mat2pmatmul  22674  decpmatmullem  22714  decpmatmul  22715  decpmatmulsumfsupp  22716  pm2mpmhmlem1  22761  pm2mpmhmlem2  22762  chfacfisf  22797  chfacfscmulgsum  22803  chfacfpmmulcl  22804  chfacfpmmulgsum  22807  chfacfpmmulgsum2  22808  cayhamlem1  22809  cpmadugsumlemF  22819  cayhamlem4  22831  nrgdsdi  24609  nrgdsdir  24610  nrginvrcnlem  24635  mdegmullem  26040  coe1mul3  26061  deg1mul2  26076  deg1mul3  26078  deg1mul3le  26079  ply1domn  26086  ply1divmo  26098  ply1divex  26099  uc1pmon1p  26114  r1pcl  26121  r1pid  26123  dvdsq1p  26125  dvdsr1p  26126  ply1rem  26128  dchrelbas3  27206  dchrmulcl  27217  dchrinv  27229  abvcxp  27583  ornglmulle  33332  orngrmulle  33333  ornglmullt  33334  orngrmullt  33335  orngmullt  33336  elrspunidl  33448  rhmimaidl  33452  isprmidlc  33467  qsidomlem1  33472  qsidomlem2  33473  mxidlprm  33490  drgextlsp  33638  fedgmullem1  33674  fedgmullem2  33675  fedgmul  33676  extdg1id  33712  mdetpmtr1  33859  matunitlindflem1  37645  matunitlindflem2  37646  lflnegcl  39098  lflvscl  39100  lkrlsp  39125  ldualvsass  39164  lclkrlem2m  41543  lclkrlem2o  41545  lclkrlem2p  41546  lcfrlem2  41567  lcfrlem3  41568  lcfrlem29  41595  mapdpglem30  41726  hdmapglem7  41953  evlsmulval  42567  mhphf  42595  hbtlem2  43123  mendlmod  43188  mendassa  43189  mon1psubm  43198  deg1mhm  43199  mnringmulrcld  44227  lidldomn1  48186  ply1mulgsum  48346  lincscm  48386  lincscmcl  48388  lincresunitlem2  48432  lmod1lem4  48446