Theorem subrgring 20806

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  ‘cfv 6531  (class class class)co 7412  Basecbs 17367   ↾_s cress 17388  1_rcur 20387  Ringcrg 20439  SubRingcsubrg 20801

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  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 6487  df-fun 6533  df-fv 6539  df-ov 7415  df-subrg 20802

This theorem is used by:  subrgcrng  20807  subrgsubg  20809  subrg1  20814  subrgsubm  20817  subrguss  20819  subrginv  20820  subrgunit  20822  subrgugrp  20823  subrgnzr  20826  subsubrg  20830  resrhm  20833  resrhm2b  20834  issubdrg  21017  imadrhmcl  21034  subdrgint  21040  abvres  21068  sralmod  21442  ring2idlqus  21585  gzrngunitlem  21718  gzrngunit  21719  issubassa3  22154  subrgpsr  22265  mplring  22306  subrgmvrf  22323  subrgascl  22355  subrgasclcl  22356  evlssca  22383  evlsvar  22384  evlsgsumadd  22385  evlsvarpw  22388  mpfconst  22398  mpfproj  22399  mpfsubrg  22400  evlsscaval  22415  evlsvarval  22416  evlsmaprhm  22420  gsumply1subr  22531  ply1ring  22545  evls1sca  22621  evls1gsumadd  22622  evls1varpw  22625  evls1varpwval  22666  evls1fpws  22667  evls1addd  22669  evls1muld  22670  asclply1subcl  22672  evls1maplmhm  22675  dmatcrng  22797  scmatcrng  22816  scmatsgrp1  22817  scmatsrng1  22818  scmatmhm  22829  scmatrhm  22830  m2cpmrhm  23044  isclmp  25398  reefgim  26759  amgmlem  27299  cntrcrng  33624  ressply1evls1  34079  ressply10g  34081  evls1subd  34086  evls1monply1  34093  vr1nz  34107  evls1fldgencl  34284  0ringirng  34303  extdgfialglem2  34307  ply1annnr  34317  irngnminplynz  34326  minplyelirng  34329  algextdeglem6  34336  imacrhmcl  43546  evlsbagval  43576  amgmwlem  50931