Theorem ringcld 20399

Description: Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.)

Hypotheses

Ref	Expression
ringcld.b	⊢ 𝐵 = (Base‘𝑅)
ringcld.t	⊢ · = (.r‘𝑅)
ringcld.r	⊢ (𝜑 → 𝑅 ∈ Ring)
ringcld.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
ringcld.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

Assertion

Ref	Expression
ringcld	⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)

Proof of Theorem ringcld

Step	Hyp	Ref	Expression
1		ringcld.r	. 2 ⊢ (𝜑 → 𝑅 ∈ Ring)
2		ringcld.x	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
3		ringcld.y	. 2 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4		ringcld.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
5		ringcld.t	. . 3 ⊢ · = (.r‘𝑅)
6	4, 5	ringcl 20392	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
7	1, 2, 3, 6	syl3anc 1398	1 ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7414  Basecbs 17304  ._rcmulr 17346  Ringcrg 20375

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-nn 12261  df-2 12330  df-sets 17259  df-slot 17277  df-ndx 17289  df-base 17305  df-plusg 17358  df-mgm 18733  df-sgrp 18824  df-mnd 18840  df-mgp 20277  df-ring 20377

This theorem is used by:  crng4  20403  gsumdixp  20462  xpsring1d  20477  rspsn0  21438  rhmqusnsg  21491  rngqiprnglin  21508  ssdifidlprm  21552  prmidlsubm  21553  frlmphl  21997  assa2ass  22081  assa2ass2  22082  assapropd  22089  rhmpsrlem2  22159  psrass1  22181  psrdi  22182  psrass23l  22184  psrass23  22186  evlsvvval  22312  evlmulval  22323  rhmcomulmpl  22343  evlsmaprhm  22350  selvvvval  22361  selvmul  22363  mhpmulcl  22380  psdmul  22397  evls1fpws  22597  evls1muld  22600  evls1maprhm  22604  rhmmpl  22608  mamuass  22627  mamuvs1  22630  mamuvs2  22631  mavmulass  22774  mdetrsca  22828  r1pid2  26390  gsummulsubdishift1  33511  gsummulsubdishift2  33512  fxpsubrg  33617  elrgspnlem2  33686  elrgspnsubrunlem1  33690  erlbr2d  33707  erler  33708  erld2  33709  rlocaddval  33712  rlocmulval  33713  rloccring  33714  rlocf1  33717  rlocisunit  33719  rrgsubm  33727  fracerl  33750  fracfld  33752  dvdsruasso  33821  rhmquskerlem  33856  elrspunsn  33860  mxidlirredi  33877  qsdrngilem  33899  dflringlem2  33908  rprmasso2  33939  unitmulrprm  33941  rprmirredlem  33943  1arithidomlem1  33948  1arithidomlem2  33949  1arithidom  33950  1arithufdlem2  33958  1arithufdlem3  33959  evl1deg1  33989  evl1deg2  33990  evl1deg3  33991  ply1dg1rt  33993  ply1mulrtss  33995  q1pdir  34016  q1pvsca  34017  r1pvsca  34018  r1pcyc  34020  r1padd1  34021  0mplrim  34027  selvply1rhmlemb  34032  selvply1rhm  34038  evlextv  34055  mplvrpmrhm  34060  psrmonmul  34063  esplyind  34088  esplyfvn  34090  vietalem  34092  srapwov  34102  assalactf1o  34148  fldextrspunlsplem  34186  fldextrspunlsp  34187  irredminply  34229  rtelextdg2lem  34239  cos9thpiminplylem6  34300  cos9thpiminply  34301  ply1divalg3  36224  r1peuqusdeg1  36225  aks6d1c1p4  42980  drnginvmuld  43412  rhmcomulpsr  43431  rhmpsr  43432  evlsbagval  43435  evlselv  43438  evlsmhpvvval  43444  mhphf  43446  prjspertr  43454  prjspner1  43475  idomcanl  49265