Theorem subrgring 20443

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3899  ‘cfv 6476  (class class class)co 7340  Basecbs 17107   ↾_s cress 17128  1_rcur 20053  Ringcrg 20105  SubRingcsubrg 20438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-iota 6432  df-fun 6478  df-fv 6484  df-ov 7343  df-subrg 20439

This theorem is referenced by:  subrgcrng  20444  subrgsubg  20446  subrg1  20451  subrgsubm  20454  subrguss  20456  subrginv  20457  subrgunit  20459  subrgugrp  20460  subrgnzr  20463  subsubrg  20467  resrhm  20470  resrhm2b  20471  issubdrg  20649  imadrhmcl  20666  subdrgint  20672  abvres  20700  sralmod  21075  ring2idlqus  21200  gzrngunitlem  21323  gzrngunit  21324  issubassa3  21757  subrgpsr  21869  mplring  21910  subrgmvrf  21923  subrgascl  21955  subrgasclcl  21956  evlssca  21978  evlsvar  21979  evlsgsumadd  21980  evlsvarpw  21983  mpfconst  21990  mpfproj  21991  mpfsubrg  21992  gsumply1subr  22100  ply1ring  22114  evls1sca  22192  evls1gsumadd  22193  evls1varpw  22196  evls1varpwval  22237  evls1fpws  22238  evls1addd  22240  evls1muld  22241  asclply1subcl  22243  evls1maplmhm  22246  dmatcrng  22371  scmatcrng  22390  scmatsgrp1  22391  scmatsrng1  22392  scmatmhm  22403  scmatrhm  22404  m2cpmrhm  22615  isclmp  24978  reefgim  26341  amgmlem  26881  cntrcrng  33018  ressply1evls1  33496  ressply10g  33498  evls1subd  33503  evls1monply1  33510  vr1nz  33522  evls1fldgencl  33651  0ringirng  33670  extdgfialglem2  33674  ply1annnr  33684  irngnminplynz  33693  minplyelirng  33696  algextdeglem6  33703  imacrhmcl  42504  evlsscaval  42554  evlsvarval  42555  evlsbagval  42556  evlsmaprhm  42560  amgmwlem  49801