Theorem subrgring 20710

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ⊆ wss 3908  ‘cfv 6543  (class class class)co 7423  Basecbs 17294   ↾_s cress 17315  1_rcur 20294  Ringcrg 20346  SubRingcsubrg 20705

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-subrg 20706

This theorem is used by:  subrgcrng  20711  subrgsubg  20713  subrg1  20718  subrgsubm  20721  subrguss  20723  subrginv  20724  subrgunit  20726  subrgugrp  20727  subrgnzr  20730  subsubrg  20734  resrhm  20737  resrhm2b  20738  issubdrg  20920  imadrhmcl  20937  subdrgint  20943  abvres  20971  sralmod  21345  ring2idlqus  21486  gzrngunitlem  21619  gzrngunit  21620  issubassa3  22053  subrgpsr  22164  mplring  22205  subrgmvrf  22222  subrgascl  22254  subrgasclcl  22255  evlssca  22282  evlsvar  22283  evlsgsumadd  22284  evlsvarpw  22287  mpfconst  22297  mpfproj  22298  mpfsubrg  22299  evlsscaval  22314  evlsvarval  22315  evlsmaprhm  22319  gsumply1subr  22430  ply1ring  22444  evls1sca  22520  evls1gsumadd  22521  evls1varpw  22524  evls1varpwval  22565  evls1fpws  22566  evls1addd  22568  evls1muld  22569  asclply1subcl  22571  evls1maplmhm  22574  dmatcrng  22696  scmatcrng  22715  scmatsgrp1  22716  scmatsrng1  22717  scmatmhm  22728  scmatrhm  22729  m2cpmrhm  22940  isclmp  25293  reefgim  26650  amgmlem  27191  cntrcrng  33432  ressply1evls1  33886  ressply10g  33888  evls1subd  33893  evls1monply1  33900  vr1nz  33914  evls1fldgencl  34091  0ringirng  34110  extdgfialglem2  34114  ply1annnr  34124  irngnminplynz  34133  minplyelirng  34136  algextdeglem6  34143  imacrhmcl  43329  evlsbagval  43359  amgmwlem  50691