Theorem subrgring 19531

Description: A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Hypothesis

Ref	Expression
subrgring.1	⊢ 𝑆 = (𝑅 ↾s 𝐴)

Assertion

Ref	Expression
subrgring	⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)

Proof of Theorem subrgring

Step	Hyp	Ref	Expression
1		subrgring.1	. 2 ⊢ 𝑆 = (𝑅 ↾s 𝐴)
2		eqid 2798	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		eqid 2798	. . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅)
4	2, 3	issubrg 19528	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐴)))
5	4	simplbi 501	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring))
6	5	simprd 499	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
7	1, 6	eqeltrid 2894	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  ‘cfv 6324  (class class class)co 7135  Basecbs 16475   ↾_s cress 16476  1_rcur 19244  Ringcrg 19290  SubRingcsubrg 19524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fv 6332  df-ov 7138  df-subrg 19526

This theorem is referenced by:  subrgcrng  19532  subrgsubg  19534  subrg1  19538  subrgmcl  19540  subrgsubm  19541  subrguss  19543  subrginv  19544  subrgunit  19546  subrgugrp  19547  issubdrg  19553  subsubrg  19554  resrhm  19557  subdrgint  19575  abvres  19603  sralmod  19952  subrgnzr  20034  gzrngunitlem  20156  gzrngunit  20157  issubassa3  20554  subrgpsr  20657  mplring  20691  subrgmvrf  20702  subrgascl  20737  subrgasclcl  20738  evlssca  20761  evlsvar  20762  evlsgsumadd  20763  evlsvarpw  20766  mpfconst  20773  mpfproj  20774  mpfsubrg  20775  gsumply1subr  20863  ply1ring  20877  evls1sca  20947  evls1gsumadd  20948  evls1varpw  20951  dmatcrng  21107  scmatcrng  21126  scmatsgrp1  21127  scmatsrng1  21128  scmatmhm  21139  scmatrhm  21140  scmatrngiso  21141  m2cpmrhm  21351  isclmp  23702  reefgim  25045  amgmlem  25575  cntrcrng  30747  amgmwlem  45330