Theorem ringcl 18561

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	|- B = ( Base ` R )
ringcl.t	|- .x. = ( .r ` R )

Assertion

Ref	Expression
ringcl	|- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )

Proof of Theorem ringcl

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- (mulGrp ` R ) = (mulGrp ` R )
2	1	ringmgp 18553	. 2 |- ( R e. Ring -> (mulGrp ` R ) e. Mnd )
3		ringcl.b	. . . 4 |- B = ( Base ` R )
4	1, 3	mgpbas 18495	. . 3 |- B = ( Base ` (mulGrp ` R ) )
5		ringcl.t	. . . 4 |- .x. = ( .r ` R )
6	1, 5	mgpplusg 18493	. . 3 |- .x. = ( +g ` (mulGrp ` R ) )
7	4, 6	mndcl 17301	. 2 |- ( ( (mulGrp ` R ) e. Mnd /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
8	2, 7	syl3an1 1359	1 |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )

Syntax hints:   -> wi 4   /\ w3a 1037   = wceq 1483   e. wcel 1990   ` cfv 5888  (class class class)co 6650   Basecbs 15857   .rcmulr 15942   Mndcmnd 17294  mulGrpcmgp 18489   Ringcrg 18547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-plusg 15954  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mgp 18490  df-ring 18549

This theorem is referenced by:  ringlz  18587  ringrz  18588  ringnegl  18594  rngnegr  18595  ringmneg1  18596  ringmneg2  18597  ringm2neg  18598  ringsubdi  18599  rngsubdir  18600  mulgass2  18601  ringlghm  18604  ringrghm  18605  gsumdixp  18609  prdsmulrcl  18611  imasring  18619  qusring2  18620  opprring  18631  dvdsrcl2  18650  dvdsrtr  18652  dvdsrmul1  18653  dvrcl  18686  dvrass  18690  irredrmul  18707  isdrngd  18772  subrgmcl  18792  abvtrivd  18840  srngmul  18858  issrngd  18861  idsrngd  18862  lmodmcl  18875  lmodprop2d  18925  rmodislmodlem  18930  prdslmodd  18969  sralmod  19187  2idlcpbl  19234  qusrhm  19237  quscrng  19240  assa2ass  19322  assapropd  19327  asclrhm  19342  psrmulcllem  19387  psrvscacl  19393  psrlmod  19401  psrlidm  19403  psrridm  19404  psrass1  19405  psrdi  19406  psrdir  19407  psrass23l  19408  psrcom  19409  psrass23  19410  mplmonmul  19464  mplmon2mul  19501  mplind  19502  evlslem2  19512  evlslem6  19513  evlslem3  19514  evlslem1  19515  mpfind  19536  psropprmul  19608  coe1mul2  19639  coe1tmmul2  19646  coe1tmmul  19647  evl1muld  19707  frlmphl  20120  mamucl  20207  mamuass  20208  mamudi  20209  mamudir  20210  mamuvs1  20211  mamuvs2  20212  mamulid  20247  mamurid  20248  madetsmelbas  20270  madetsmelbas2  20271  mat1dimscm  20281  mat1dimmul  20282  mat1mhm  20290  dmatmul  20303  dmatmulcl  20306  scmatscmiddistr  20314  scmatscm  20319  scmatmulcl  20324  smatvscl  20330  scmatmhm  20340  mavmulcl  20353  mavmulass  20355  mdetleib2  20394  mdetf  20401  mdetrlin  20408  mdetrsca  20409  mdetrsca2  20410  mdetralt  20414  mdetero  20416  mdetuni0  20427  mdetmul  20429  m2detleib  20437  madugsum  20449  madulid  20451  cpmatmcllem  20523  cpmatmcl  20524  mat2pmatmul  20536  decpmatmullem  20576  decpmatmul  20577  decpmatmulsumfsupp  20578  pm2mpmhmlem1  20623  pm2mpmhmlem2  20624  chfacfisf  20659  chfacfscmulgsum  20665  chfacfpmmulcl  20666  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmadugsumlemF  20681  cayhamlem4  20693  nrgdsdi  22469  nrgdsdir  22470  nrginvrcnlem  22495  mdegmullem  23838  coe1mul3  23859  deg1mul2  23874  deg1mul3  23875  deg1mul3le  23876  ply1domn  23883  ply1divmo  23895  ply1divex  23896  uc1pmon1p  23911  r1pcl  23917  r1pid  23919  dvdsq1p  23920  dvdsr1p  23921  ply1rem  23923  dchrelbas3  24963  dchrmulcl  24974  dchrinv  24986  abvcxp  25304  rdivmuldivd  29791  ornglmulle  29805  orngrmulle  29806  ornglmullt  29807  orngrmullt  29808  orngmullt  29809  mdetpmtr1  29889  matunitlindflem1  33405  matunitlindflem2  33406  lflnegcl  34362  lflvscl  34364  lkrlsp  34389  ldualvsass  34428  lclkrlem2m  36808  lclkrlem2o  36810  lclkrlem2p  36811  lcfrlem2  36832  lcfrlem3  36833  lcfrlem29  36860  mapdpglem30  36991  hdmapglem7  37221  hbtlem2  37694  mendlmod  37763  mendassa  37764  isdomn3  37782  mon1psubm  37784  deg1mhm  37785  lidldomn1  41921  ply1mulgsum  42178  lincscm  42219  lincscmcl  42221  lincresunitlem2  42265  lmod1lem4  42279