Theorem subrgring 20591

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106   ⊆ wss 3963  ‘cfv 6563  (class class class)co 7431  Basecbs 17245   ↾_s cress 17274  1_rcur 20199  Ringcrg 20251  SubRingcsubrg 20586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-subrg 20587

This theorem is referenced by:  subrgcrng  20592  subrgsubg  20594  subrg1  20599  subrgsubm  20602  subrguss  20604  subrginv  20605  subrgunit  20607  subrgugrp  20608  subrgnzr  20611  subsubrg  20615  resrhm  20618  resrhm2b  20619  issubdrg  20798  imadrhmcl  20815  subdrgint  20821  abvres  20849  sralmod  21212  ring2idlqus  21337  gzrngunitlem  21468  gzrngunit  21469  issubassa3  21904  subrgpsr  22016  mplring  22057  subrgmvrf  22070  subrgascl  22108  subrgasclcl  22109  evlssca  22131  evlsvar  22132  evlsgsumadd  22133  evlsvarpw  22136  mpfconst  22143  mpfproj  22144  mpfsubrg  22145  gsumply1subr  22251  ply1ring  22265  evls1sca  22343  evls1gsumadd  22344  evls1varpw  22347  evls1varpwval  22388  evls1fpws  22389  evls1addd  22391  evls1muld  22392  asclply1subcl  22394  evls1maplmhm  22397  dmatcrng  22524  scmatcrng  22543  scmatsgrp1  22544  scmatsrng1  22545  scmatmhm  22556  scmatrhm  22557  m2cpmrhm  22768  isclmp  25144  reefgim  26509  amgmlem  27048  cntrcrng  33056  ressply10g  33572  evls1subd  33577  evls1fldgencl  33695  0ringirng  33704  ply1annnr  33711  irngnminplynz  33720  algextdeglem6  33728  imacrhmcl  42501  evlsscaval  42551  evlsvarval  42552  evlsbagval  42553  evlsmaprhm  42557  amgmwlem  49033