Theorem subrgring 20647

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ⊆ wss 3907  ‘cfv 6525  (class class class)co 7400  Basecbs 17257   ↾_s cress 17278  1_rcur 20251  Ringcrg 20303  SubRingcsubrg 20642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-subrg 20643

This theorem is referenced by:  subrgcrng  20648  subrgsubg  20650  subrg1  20655  subrgsubm  20658  subrguss  20660  subrginv  20661  subrgunit  20663  subrgugrp  20664  subrgnzr  20667  subsubrg  20671  resrhm  20674  resrhm2b  20675  issubdrg  20849  imadrhmcl  20866  subdrgint  20872  abvres  20900  sralmod  21274  ring2idlqus  21408  gzrngunitlem  21539  gzrngunit  21540  issubassa3  21973  subrgpsr  22084  mplring  22125  subrgmvrf  22142  subrgascl  22174  subrgasclcl  22175  evlssca  22202  evlsvar  22203  evlsgsumadd  22204  evlsvarpw  22207  mpfconst  22217  mpfproj  22218  mpfsubrg  22219  evlsscaval  22234  evlsvarval  22235  evlsmaprhm  22239  gsumply1subr  22350  ply1ring  22364  evls1sca  22440  evls1gsumadd  22441  evls1varpw  22444  evls1varpwval  22485  evls1fpws  22486  evls1addd  22488  evls1muld  22489  asclply1subcl  22491  evls1maplmhm  22494  dmatcrng  22616  scmatcrng  22635  scmatsgrp1  22636  scmatsrng1  22637  scmatmhm  22648  scmatrhm  22649  m2cpmrhm  22860  isclmp  25213  reefgim  26567  amgmlem  27108  cntrcrng  33309  ressply1evls1  33767  ressply10g  33769  evls1subd  33774  evls1monply1  33781  vr1nz  33795  evls1fldgencl  33972  0ringirng  33991  extdgfialglem2  33995  ply1annnr  34005  irngnminplynz  34014  minplyelirng  34017  algextdeglem6  34024  imacrhmcl  43143  evlsbagval  43175  amgmwlem  50432