Theorem ringacl 20366

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

Step	Hyp	Ref	Expression
1		ringgrp 20324	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2		ringacl.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
3		ringacl.p	. . 3 ⊢ + = (+g‘𝑅)
4	2, 3	grpcl 19012	. 2 ⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
5	1, 4	syl3an1 1181	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  Basecbs 17273  +_gcplusg 17314  Grpcgrp 19004  Ringcrg 20319

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-mgm 18702  df-sgrp 18781  df-mnd 18797  df-grp 19007  df-ring 20321

This theorem is used by:  ringcomlem  20367  ringcom  20368  ringlghm  20400  ringrghm  20401  imasring  20417  qusring2  20421  cntzsubr  20714  srngadd  20963  issrngd  20967  lmodprop2d  21054  prdslmodd  21099  rhmpreimaidl  21425  frobrhm  21734  ip2subdi  21803  psrlmod  22118  mpfind  22275  coe1add  22434  mat1ghm  22649  scmatghm  22699  mdetrlin2  22773  mdetunilem5  22782  cpmatacl  22882  mdegaddle  26240  deg1addle2  26268  deg1add  26269  ply1divex  26303  deg1addlt  33899  dvhlveclem  41910  baerlem3lem1  42509  mendlmod  43944  cznrng  49054  lmod1lem3  49297