Theorem subrgring 19606

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 2758	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		eqid 2758	. . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅)
4	2, 3	issubrg 19603	. . . 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 2856	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ⊆ wss 3858  ‘cfv 6335  (class class class)co 7150  Basecbs 16541   ↾_s cress 16542  1_rcur 19319  Ringcrg 19365  SubRingcsubrg 19599

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 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fv 6343  df-ov 7153  df-subrg 19601

This theorem is referenced by:  subrgcrng  19607  subrgsubg  19609  subrg1  19613  subrgmcl  19615  subrgsubm  19616  subrguss  19618  subrginv  19619  subrgunit  19621  subrgugrp  19622  issubdrg  19628  subsubrg  19629  resrhm  19632  subdrgint  19650  abvres  19678  sralmod  20027  subrgnzr  20109  gzrngunitlem  20231  gzrngunit  20232  issubassa3  20630  subrgpsr  20747  mplring  20783  subrgmvrf  20794  subrgascl  20827  subrgasclcl  20828  evlssca  20852  evlsvar  20853  evlsgsumadd  20854  evlsvarpw  20857  mpfconst  20864  mpfproj  20865  mpfsubrg  20866  gsumply1subr  20958  ply1ring  20972  evls1sca  21042  evls1gsumadd  21043  evls1varpw  21046  dmatcrng  21202  scmatcrng  21221  scmatsgrp1  21222  scmatsrng1  21223  scmatmhm  21234  scmatrhm  21235  scmatrngiso  21236  m2cpmrhm  21446  isclmp  23798  reefgim  25144  amgmlem  25674  cntrcrng  30848  evlsscaval  39778  evlsvarval  39779  evlsbagval  39780  mhphf  39790  amgmwlem  45721