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

Theorem ringacl 18799
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 18773 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 ringacl.b . . 3 𝐵 = (Base‘𝑅)
3 ringacl.p . . 3 + = (+g𝑅)
42, 3grpcl 17652 . 2 ((𝑅 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
51, 4syl3an1 1167 1 ((𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1632  wcel 2140  cfv 6050  (class class class)co 6815  Basecbs 16080  +gcplusg 16164  Grpcgrp 17644  Ringcrg 18768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-nul 4942
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818  df-mgm 17464  df-sgrp 17506  df-mnd 17517  df-grp 17647  df-ring 18770
This theorem is referenced by:  ringcom  18800  ringlghm  18825  ringrghm  18826  imasring  18840  qusring2  18841  cntzsubr  19035  srngadd  19080  issrngd  19084  lmodprop2d  19148  prdslmodd  19192  psrlmod  19624  mpfind  19759  coe1add  19857  ip2subdi  20212  mat1ghm  20512  scmatghm  20562  mdetrlin2  20636  mdetunilem5  20645  cpmatacl  20744  mdegaddle  24054  deg1addle2  24082  deg1add  24083  ply1divex  24116  dvhlveclem  36918  baerlem3lem1  37517  mendlmod  38284  cznrng  42484  lmod1lem3  42807
  Copyright terms: Public domain W3C validator