Theorem subrgring 20465

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105   ⊆ wss 3948  ‘cfv 6543  (class class class)co 7412  Basecbs 17149   ↾_s cress 17178  1_rcur 20076  Ringcrg 20128  SubRingcsubrg 20458

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7415  df-subrg 20460

This theorem is referenced by:  subrgcrng  20466  subrgsubg  20468  subrg1  20473  subrgsubm  20476  subrguss  20478  subrginv  20479  subrgunit  20481  subrgugrp  20482  subrgnzr  20485  subsubrg  20489  resrhm  20492  resrhm2b  20493  issubdrg  20545  imadrhmcl  20557  subdrgint  20563  abvres  20591  sralmod  20955  ring2idlqus  21069  gzrngunitlem  21211  gzrngunit  21212  issubassa3  21640  subrgpsr  21759  mplring  21798  subrgmvrf  21809  subrgascl  21847  subrgasclcl  21848  evlssca  21872  evlsvar  21873  evlsgsumadd  21874  evlsvarpw  21877  mpfconst  21884  mpfproj  21885  mpfsubrg  21886  gsumply1subr  21977  ply1ring  21991  evls1sca  22063  evls1gsumadd  22064  evls1varpw  22067  dmatcrng  22225  scmatcrng  22244  scmatsgrp1  22245  scmatsrng1  22246  scmatmhm  22257  scmatrhm  22258  m2cpmrhm  22469  isclmp  24845  reefgim  26199  amgmlem  26731  cntrcrng  32485  evls1varpwval  32920  evls1fpws  32921  evls1addd  32923  evls1muld  32924  ressply10g  32931  asclply1subcl  32935  evls1fldgencl  33034  0ringirng  33043  evls1maplmhm  33050  ply1annnr  33054  irngnminplynz  33061  algextdeglem6  33068  imacrhmcl  41394  evlsscaval  41439  evlsvarval  41440  evlsbagval  41441  evlsmaprhm  41445  amgmwlem  47937