Theorem subrgring 20507

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  ‘cfv 6492  (class class class)co 7358  Basecbs 17136   ↾_s cress 17157  1_rcur 20116  Ringcrg 20168  SubRingcsubrg 20502

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-subrg 20503

This theorem is referenced by:  subrgcrng  20508  subrgsubg  20510  subrg1  20515  subrgsubm  20518  subrguss  20520  subrginv  20521  subrgunit  20523  subrgugrp  20524  subrgnzr  20527  subsubrg  20531  resrhm  20534  resrhm2b  20535  issubdrg  20713  imadrhmcl  20730  subdrgint  20736  abvres  20764  sralmod  21139  ring2idlqus  21264  gzrngunitlem  21387  gzrngunit  21388  issubassa3  21821  subrgpsr  21933  mplring  21974  subrgmvrf  21989  subrgascl  22021  subrgasclcl  22022  evlssca  22049  evlsvar  22050  evlsgsumadd  22051  evlsvarpw  22054  mpfconst  22064  mpfproj  22065  mpfsubrg  22066  gsumply1subr  22174  ply1ring  22188  evls1sca  22267  evls1gsumadd  22268  evls1varpw  22271  evls1varpwval  22312  evls1fpws  22313  evls1addd  22315  evls1muld  22316  asclply1subcl  22318  evls1maplmhm  22321  dmatcrng  22446  scmatcrng  22465  scmatsgrp1  22466  scmatsrng1  22467  scmatmhm  22478  scmatrhm  22479  m2cpmrhm  22690  isclmp  25053  reefgim  26416  amgmlem  26956  cntrcrng  33163  ressply1evls1  33646  ressply10g  33648  evls1subd  33653  evls1monply1  33660  vr1nz  33674  evls1fldgencl  33827  0ringirng  33846  extdgfialglem2  33850  ply1annnr  33860  irngnminplynz  33869  minplyelirng  33872  algextdeglem6  33879  imacrhmcl  42769  evlsscaval  42810  evlsvarval  42811  evlsbagval  42812  evlsmaprhm  42816  amgmwlem  50047