Theorem subrgring 20493

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3898  ‘cfv 6488  (class class class)co 7354  Basecbs 17124   ↾_s cress 17145  1_rcur 20103  Ringcrg 20155  SubRingcsubrg 20488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fv 6496  df-ov 7357  df-subrg 20489

This theorem is referenced by:  subrgcrng  20494  subrgsubg  20496  subrg1  20501  subrgsubm  20504  subrguss  20506  subrginv  20507  subrgunit  20509  subrgugrp  20510  subrgnzr  20513  subsubrg  20517  resrhm  20520  resrhm2b  20521  issubdrg  20699  imadrhmcl  20716  subdrgint  20722  abvres  20750  sralmod  21125  ring2idlqus  21250  gzrngunitlem  21373  gzrngunit  21374  issubassa3  21807  subrgpsr  21918  mplring  21959  subrgmvrf  21972  subrgascl  22004  subrgasclcl  22005  evlssca  22027  evlsvar  22028  evlsgsumadd  22029  evlsvarpw  22032  mpfconst  22039  mpfproj  22040  mpfsubrg  22041  gsumply1subr  22149  ply1ring  22163  evls1sca  22241  evls1gsumadd  22242  evls1varpw  22245  evls1varpwval  22286  evls1fpws  22287  evls1addd  22289  evls1muld  22290  asclply1subcl  22292  evls1maplmhm  22295  dmatcrng  22420  scmatcrng  22439  scmatsgrp1  22440  scmatsrng1  22441  scmatmhm  22452  scmatrhm  22453  m2cpmrhm  22664  isclmp  25027  reefgim  26390  amgmlem  26930  cntrcrng  33059  ressply1evls1  33537  ressply10g  33539  evls1subd  33544  evls1monply1  33551  vr1nz  33563  evls1fldgencl  33706  0ringirng  33725  extdgfialglem2  33729  ply1annnr  33739  irngnminplynz  33748  minplyelirng  33751  algextdeglem6  33758  imacrhmcl  42635  evlsscaval  42685  evlsvarval  42686  evlsbagval  42687  evlsmaprhm  42691  amgmwlem  49930