Theorem subrgring 20832

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 2760	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		eqid 2760	. . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅)
4	2, 3	issubrg 20829	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐴)))
5	4	simplbi 502	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring))
6	5	simprd 501	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
7	1, 6	eqeltrid 2864	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  ‘cfv 6539  (class class class)co 7421  Basecbs 17393   ↾_s cress 17414  1_rcur 20413  Ringcrg 20465  SubRingcsubrg 20827

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fv 6547  df-ov 7424  df-subrg 20828

This theorem is used by:  subrgcrng  20833  subrgsubg  20835  subrg1  20840  subrgsubm  20843  subrguss  20845  subrginv  20846  subrgunit  20848  subrgugrp  20849  subrgnzr  20852  subsubrg  20856  resrhm  20859  resrhm2b  20860  issubdrg  21043  imadrhmcl  21060  subdrgint  21066  abvres  21094  sralmod  21468  ring2idlqus  21611  gzrngunitlem  21744  gzrngunit  21745  issubassa3  22180  subrgpsr  22291  mplring  22332  subrgmvrf  22349  subrgascl  22381  subrgasclcl  22382  evlssca  22409  evlsvar  22410  evlsgsumadd  22411  evlsvarpw  22414  mpfconst  22424  mpfproj  22425  mpfsubrg  22426  evlsscaval  22441  evlsvarval  22442  evlsmaprhm  22446  gsumply1subr  22557  ply1ring  22571  evls1sca  22647  evls1gsumadd  22648  evls1varpw  22651  evls1varpwval  22692  evls1fpws  22693  evls1addd  22695  evls1muld  22696  asclply1subcl  22698  evls1maplmhm  22701  dmatcrng  22823  scmatcrng  22842  scmatsgrp1  22843  scmatsrng1  22844  scmatmhm  22855  scmatrhm  22856  m2cpmrhm  23070  isclmp  25424  reefgim  26783  amgmlem  27323  cntrcrng  33689  ressply1evls1  34144  ressply10g  34146  evls1subd  34151  evls1monply1  34158  vr1nz  34172  evls1fldgencl  34349  0ringirng  34368  extdgfialglem2  34372  ply1annnr  34382  irngnminplynz  34391  minplyelirng  34394  algextdeglem6  34401  imacrhmcl  43675  evlsbagval  43708  amgmwlem  51156