Theorem subrgring 20742

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ⊆ wss 3902  ‘cfv 6537  (class class class)co 7417  Basecbs 17307   ↾_s cress 17328  1_rcur 20326  Ringcrg 20378  SubRingcsubrg 20737

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-subrg 20738

This theorem is used by:  subrgcrng  20743  subrgsubg  20745  subrg1  20750  subrgsubm  20753  subrguss  20755  subrginv  20756  subrgunit  20758  subrgugrp  20759  subrgnzr  20762  subsubrg  20766  resrhm  20769  resrhm2b  20770  issubdrg  20952  imadrhmcl  20969  subdrgint  20975  abvres  21003  sralmod  21377  ring2idlqus  21518  gzrngunitlem  21651  gzrngunit  21652  issubassa3  22087  subrgpsr  22198  mplring  22239  subrgmvrf  22256  subrgascl  22288  subrgasclcl  22289  evlssca  22316  evlsvar  22317  evlsgsumadd  22318  evlsvarpw  22321  mpfconst  22331  mpfproj  22332  mpfsubrg  22333  evlsscaval  22348  evlsvarval  22349  evlsmaprhm  22353  gsumply1subr  22464  ply1ring  22478  evls1sca  22554  evls1gsumadd  22555  evls1varpw  22558  evls1varpwval  22599  evls1fpws  22600  evls1addd  22602  evls1muld  22603  asclply1subcl  22605  evls1maplmhm  22608  dmatcrng  22730  scmatcrng  22749  scmatsgrp1  22750  scmatsrng1  22751  scmatmhm  22762  scmatrhm  22763  m2cpmrhm  22977  isclmp  25331  reefgim  26693  amgmlem  27234  cntrcrng  33529  ressply1evls1  33983  ressply10g  33985  evls1subd  33990  evls1monply1  33997  vr1nz  34011  evls1fldgencl  34188  0ringirng  34207  extdgfialglem2  34211  ply1annnr  34221  irngnminplynz  34230  minplyelirng  34233  algextdeglem6  34240  imacrhmcl  43410  evlsbagval  43440  amgmwlem  50828