Theorem subrgring 20539

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3931  ‘cfv 6536  (class class class)co 7410  Basecbs 17233   ↾_s cress 17256  1_rcur 20146  Ringcrg 20198  SubRingcsubrg 20534

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 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fv 6544  df-ov 7413  df-subrg 20535

This theorem is referenced by:  subrgcrng  20540  subrgsubg  20542  subrg1  20547  subrgsubm  20550  subrguss  20552  subrginv  20553  subrgunit  20555  subrgugrp  20556  subrgnzr  20559  subsubrg  20563  resrhm  20566  resrhm2b  20567  issubdrg  20745  imadrhmcl  20762  subdrgint  20768  abvres  20796  sralmod  21150  ring2idlqus  21275  gzrngunitlem  21405  gzrngunit  21406  issubassa3  21831  subrgpsr  21943  mplring  21984  subrgmvrf  21997  subrgascl  22029  subrgasclcl  22030  evlssca  22052  evlsvar  22053  evlsgsumadd  22054  evlsvarpw  22057  mpfconst  22064  mpfproj  22065  mpfsubrg  22066  gsumply1subr  22174  ply1ring  22188  evls1sca  22266  evls1gsumadd  22267  evls1varpw  22270  evls1varpwval  22311  evls1fpws  22312  evls1addd  22314  evls1muld  22315  asclply1subcl  22317  evls1maplmhm  22320  dmatcrng  22445  scmatcrng  22464  scmatsgrp1  22465  scmatsrng1  22466  scmatmhm  22477  scmatrhm  22478  m2cpmrhm  22689  isclmp  25053  reefgim  26417  amgmlem  26957  cntrcrng  33069  ressply1evls1  33583  ressply10g  33585  evls1subd  33590  vr1nz  33608  evls1fldgencl  33716  0ringirng  33735  ply1annnr  33742  irngnminplynz  33751  minplyelirng  33754  algextdeglem6  33761  imacrhmcl  42512  evlsscaval  42562  evlsvarval  42563  evlsbagval  42564  evlsmaprhm  42568  amgmwlem  49646