Theorem subrgring 20542

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  ‘cfv 6492  (class class class)co 7360  Basecbs 17170   ↾_s cress 17191  1_rcur 20153  Ringcrg 20205  SubRingcsubrg 20537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 7363  df-subrg 20538

This theorem is referenced by:  subrgcrng  20543  subrgsubg  20545  subrg1  20550  subrgsubm  20553  subrguss  20555  subrginv  20556  subrgunit  20558  subrgugrp  20559  subrgnzr  20562  subsubrg  20566  resrhm  20569  resrhm2b  20570  issubdrg  20748  imadrhmcl  20765  subdrgint  20771  abvres  20799  sralmod  21174  ring2idlqus  21299  gzrngunitlem  21422  gzrngunit  21423  issubassa3  21856  subrgpsr  21966  mplring  22007  subrgmvrf  22022  subrgascl  22054  subrgasclcl  22055  evlssca  22082  evlsvar  22083  evlsgsumadd  22084  evlsvarpw  22087  mpfconst  22097  mpfproj  22098  mpfsubrg  22099  gsumply1subr  22207  ply1ring  22221  evls1sca  22298  evls1gsumadd  22299  evls1varpw  22302  evls1varpwval  22343  evls1fpws  22344  evls1addd  22346  evls1muld  22347  asclply1subcl  22349  evls1maplmhm  22352  dmatcrng  22477  scmatcrng  22496  scmatsgrp1  22497  scmatsrng1  22498  scmatmhm  22509  scmatrhm  22510  m2cpmrhm  22721  isclmp  25074  reefgim  26428  amgmlem  26967  cntrcrng  33157  ressply1evls1  33640  ressply10g  33642  evls1subd  33647  evls1monply1  33654  vr1nz  33668  evls1fldgencl  33830  0ringirng  33849  extdgfialglem2  33853  ply1annnr  33863  irngnminplynz  33872  minplyelirng  33875  algextdeglem6  33882  imacrhmcl  42973  evlsscaval  43014  evlsvarval  43015  evlsbagval  43016  evlsmaprhm  43020  amgmwlem  50289