MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringacl Structured version   Visualization version   GIF version

Theorem ringacl 19601
Description: Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.)
Hypotheses
Ref Expression
ringacl.b 𝐵 = (Base‘𝑅)
ringacl.p + = (+g𝑅)
Assertion
Ref Expression
ringacl ((𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

Proof of Theorem ringacl
StepHypRef Expression
1 ringgrp 19572 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 ringacl.b . . 3 𝐵 = (Base‘𝑅)
3 ringacl.p . . 3 + = (+g𝑅)
42, 3grpcl 18378 . 2 ((𝑅 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
51, 4syl3an1 1165 1 ((𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1089   = wceq 1543  wcel 2110  cfv 6385  (class class class)co 7218  Basecbs 16765  +gcplusg 16807  Grpcgrp 18370  Ringcrg 19567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-nul 5204
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3415  df-sbc 3700  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-br 5059  df-iota 6343  df-fv 6393  df-ov 7221  df-mgm 18119  df-sgrp 18168  df-mnd 18179  df-grp 18373  df-ring 19569
This theorem is referenced by:  ringcom  19602  ringlghm  19627  ringrghm  19628  imasring  19642  qusring2  19643  cntzsubr  19838  srngadd  19898  issrngd  19902  lmodprop2d  19966  prdslmodd  20011  ip2subdi  20611  psrlmod  20931  mpfind  21072  coe1add  21190  mat1ghm  21385  scmatghm  21435  mdetrlin2  21509  mdetunilem5  21518  cpmatacl  21618  mdegaddle  24977  deg1addle2  25005  deg1add  25006  ply1divex  25039  frobrhm  31209  rhmpreimaidl  31322  dvhlveclem  38864  baerlem3lem1  39463  mendlmod  40729  cznrng  45194  lmod1lem3  45511
  Copyright terms: Public domain W3C validator