Theorem subrgring 18993

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 2771	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		eqid 2771	. . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅)
4	2, 3	issubrg 18990	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐴)))
5	4	simplbi 485	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring))
6	5	simprd 483	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
7	1, 6	syl5eqel 2854	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145   ⊆ wss 3723  ‘cfv 6031  (class class class)co 6793  Basecbs 16064   ↾_s cress 16065  1_rcur 18709  Ringcrg 18755  SubRingcsubrg 18986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fv 6039  df-ov 6796  df-subrg 18988

This theorem is referenced by:  subrgcrng  18994  subrgsubg  18996  subrg1  19000  subrgmcl  19002  subrgsubm  19003  subrguss  19005  subrginv  19006  subrgunit  19008  subrgugrp  19009  issubdrg  19015  subsubrg  19016  resrhm  19019  abvres  19049  sralmod  19402  subrgnzr  19483  issubassa  19539  subrgpsr  19634  mplring  19667  subrgmvrf  19677  subrgascl  19713  subrgasclcl  19714  evlssca  19737  evlsvar  19738  mpfconst  19745  mpfproj  19746  mpfsubrg  19747  gsumply1subr  19819  ply1ring  19833  evls1sca  19903  evls1gsumadd  19904  evls1varpw  19906  gzrngunitlem  20026  gzrngunit  20027  dmatcrng  20526  scmatcrng  20545  scmatsgrp1  20546  scmatsrng1  20547  scmatmhm  20558  scmatrhm  20559  scmatrngiso  20560  m2cpmrhm  20771  isclmp  23116  reefgim  24424  amgmlem  24937  amgmwlem  43079