MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subrgring Structured version   Visualization version   GIF version

Theorem subrgring 20221
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
StepHypRef Expression
1 subrgring.1 . 2 𝑆 = (𝑅s 𝐴)
2 eqid 2736 . . . . 5 (Base‘𝑅) = (Base‘𝑅)
3 eqid 2736 . . . . 5 (1r𝑅) = (1r𝑅)
42, 3issubrg 20218 . . . 4 (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ (Base‘𝑅) ∧ (1r𝑅) ∈ 𝐴)))
54simplbi 498 . . 3 (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ∈ Ring ∧ (𝑅s 𝐴) ∈ Ring))
65simprd 496 . 2 (𝐴 ∈ (SubRing‘𝑅) → (𝑅s 𝐴) ∈ Ring)
71, 6eqeltrid 2842 1 (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wss 3909  cfv 6494  (class class class)co 7354  Basecbs 17080  s cress 17109  1rcur 19909  Ringcrg 19960  SubRingcsubrg 20214
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5530  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6446  df-fun 6496  df-fv 6502  df-ov 7357  df-subrg 20216
This theorem is referenced by:  subrgcrng  20222  subrgsubg  20224  subrg1  20228  subrgmcl  20230  subrgsubm  20231  subrguss  20233  subrginv  20234  subrgunit  20236  subrgugrp  20237  issubdrg  20243  subsubrg  20244  resrhm  20247  subdrgint  20266  abvres  20294  sralmod  20652  subrgnzr  20734  gzrngunitlem  20858  gzrngunit  20859  issubassa3  21267  subrgpsr  21384  mplring  21420  subrgmvrf  21431  subrgascl  21470  subrgasclcl  21471  evlssca  21495  evlsvar  21496  evlsgsumadd  21497  evlsvarpw  21500  mpfconst  21507  mpfproj  21508  mpfsubrg  21509  gsumply1subr  21601  ply1ring  21615  evls1sca  21685  evls1gsumadd  21686  evls1varpw  21689  dmatcrng  21847  scmatcrng  21866  scmatsgrp1  21867  scmatsrng1  21868  scmatmhm  21879  scmatrhm  21880  m2cpmrhm  22091  isclmp  24456  reefgim  25805  amgmlem  26335  cntrcrng  31799  evls1varpwval  32161  evls1fpws  32162  evls1addd  32164  evls1muld  32165  ressply10g  32168  asclply1subcl  32172  0ringirng  32254  resrhm2b  40683  rncrhmcl  40684  evlsscaval  40724  evlsvarval  40725  evlsbagval  40726  mhphf  40747  amgmwlem  47219
  Copyright terms: Public domain W3C validator