Theorem subrgring 20610

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 20607	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐴)))
5	4	simplbi 500	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring))
6	5	simprd 499	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
7	1, 6	eqeltrid 2865	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ⊆ wss 3902  ‘cfv 6515  (class class class)co 7390  Basecbs 17235   ↾_s cress 17256  1_rcur 20217  Ringcrg 20269  SubRingcsubrg 20605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fv 6523  df-ov 7393  df-subrg 20606

This theorem is referenced by:  subrgcrng  20611  subrgsubg  20613  subrg1  20618  subrgsubm  20621  subrguss  20623  subrginv  20624  subrgunit  20626  subrgugrp  20627  subrgnzr  20630  subsubrg  20634  resrhm  20637  resrhm2b  20638  issubdrg  20816  imadrhmcl  20833  subdrgint  20839  abvres  20867  sralmod  21241  ring2idlqus  21366  gzrngunitlem  21471  gzrngunit  21472  issubassa3  21905  subrgpsr  22016  mplring  22057  subrgmvrf  22074  subrgascl  22106  subrgasclcl  22107  evlssca  22134  evlsvar  22135  evlsgsumadd  22136  evlsvarpw  22139  mpfconst  22149  mpfproj  22150  mpfsubrg  22151  evlsscaval  22166  evlsvarval  22167  evlsmaprhm  22171  gsumply1subr  22282  ply1ring  22296  evls1sca  22373  evls1gsumadd  22374  evls1varpw  22377  evls1varpwval  22418  evls1fpws  22419  evls1addd  22421  evls1muld  22422  asclply1subcl  22424  evls1maplmhm  22427  dmatcrng  22549  scmatcrng  22568  scmatsgrp1  22569  scmatsrng1  22570  scmatmhm  22581  scmatrhm  22582  m2cpmrhm  22793  isclmp  25146  reefgim  26500  amgmlem  27041  cntrcrng  33221  ressply1evls1  33721  ressply10g  33723  evls1subd  33728  evls1monply1  33735  vr1nz  33749  evls1fldgencl  33927  0ringirng  33946  extdgfialglem2  33950  ply1annnr  33960  irngnminplynz  33969  minplyelirng  33972  algextdeglem6  33979  imacrhmcl  43096  evlsbagval  43128  amgmwlem  50383