MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rngacl Structured version   Unicode version

Theorem rngacl 16694
Description: Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.)
Hypotheses
Ref Expression
rngacl.b  |-  B  =  ( Base `  R
)
rngacl.p  |-  .+  =  ( +g  `  R )
Assertion
Ref Expression
rngacl  |-  ( ( R  e.  Ring  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  e.  B )

Proof of Theorem rngacl
StepHypRef Expression
1 rnggrp 16672 . 2  |-  ( R  e.  Ring  ->  R  e. 
Grp )
2 rngacl.b . . 3  |-  B  =  ( Base `  R
)
3 rngacl.p . . 3  |-  .+  =  ( +g  `  R )
42, 3grpcl 15572 . 2  |-  ( ( R  e.  Grp  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y
)  e.  B )
51, 4syl3an1 1251 1  |-  ( ( R  e.  Ring  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965    = wceq 1369    e. wcel 1756   ` cfv 5439  (class class class)co 6112   Basecbs 14195   +g cplusg 14259   Grpcgrp 15431   Ringcrg 16667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4442  ax-pow 4491
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447  df-ov 6115  df-mnd 15436  df-grp 15566  df-rng 16669
This theorem is referenced by:  rngcom  16695  rnglghm  16715  rngrghm  16716  imasrng  16733  divsrng2  16734  cntzsubr  16919  srngadd  16964  issrngd  16968  lmodprop2d  17029  prdslmodd  17072  psrlmod  17494  mpfind  17644  coe1add  17740  ip2subdi  18095  mdetrlin2  18435  mdetunilem5  18444  mdegaddle  21567  deg1addle2  21596  deg1add  21597  ply1divex  21630  mendlmod  29576  lmod1lem3  31028  cnstpmatacl  31068  dvhlveclem  34849  baerlem3lem1  35448
  Copyright terms: Public domain W3C validator