MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subrgsubg Structured version   Unicode version

Theorem subrgsubg 16993
Description: A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
Assertion
Ref Expression
subrgsubg  |-  ( A  e.  (SubRing `  R
)  ->  A  e.  (SubGrp `  R ) )

Proof of Theorem subrgsubg
StepHypRef Expression
1 subrgrcl 16992 . . 3  |-  ( A  e.  (SubRing `  R
)  ->  R  e.  Ring )
2 rnggrp 16772 . . 3  |-  ( R  e.  Ring  ->  R  e. 
Grp )
31, 2syl 16 . 2  |-  ( A  e.  (SubRing `  R
)  ->  R  e.  Grp )
4 eqid 2454 . . 3  |-  ( Base `  R )  =  (
Base `  R )
54subrgss 16988 . 2  |-  ( A  e.  (SubRing `  R
)  ->  A  C_  ( Base `  R ) )
6 eqid 2454 . . . 4  |-  ( Rs  A )  =  ( Rs  A )
76subrgrng 16990 . . 3  |-  ( A  e.  (SubRing `  R
)  ->  ( Rs  A
)  e.  Ring )
8 rnggrp 16772 . . 3  |-  ( ( Rs  A )  e.  Ring  -> 
( Rs  A )  e.  Grp )
97, 8syl 16 . 2  |-  ( A  e.  (SubRing `  R
)  ->  ( Rs  A
)  e.  Grp )
104issubg 15799 . 2  |-  ( A  e.  (SubGrp `  R
)  <->  ( R  e. 
Grp  /\  A  C_  ( Base `  R )  /\  ( Rs  A )  e.  Grp ) )
113, 5, 9, 10syl3anbrc 1172 1  |-  ( A  e.  (SubRing `  R
)  ->  A  e.  (SubGrp `  R ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758    C_ wss 3435   ` cfv 5525  (class class class)co 6199   Basecbs 14291   ↾s cress 14292   Grpcgrp 15528  SubGrpcsubg 15793   Ringcrg 16767  SubRingcsubrg 16983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fv 5533  df-ov 6202  df-subg 15796  df-rng 16769  df-subrg 16985
This theorem is referenced by:  subrg0  16994  subrgbas  16996  subrgacl  16998  issubrg2  17007  subrgint  17009  resrhm  17016  rhmima  17018  abvres  17046  issubassa2  17537  resspsrmul  17612  subrgpsr  17614  mplbas2  17674  mplbas2OLD  17675  gsumply1subr  17811  zsssubrg  17995  gzrngunitlem  18001  zringlpirlem1  18027  zringcyg  18031  zlpirlem1  18032  zcyg  18036  prmirred  18043  prmirredOLD  18046  expghmOLD  18048  mulgrhm2OLD  18054  zndvds  18106  resubgval  18163  subrgnrg  20385  sranlm  20396  clmsub  20783  clmneg  20784  clmabs  20785  clmsubcl  20788  cphsqrcl3  20837  tchcph  20883  plypf1  21812  dvply2g  21883  taylply2  21965  jensenlem2  22513  amgmlem  22515  lgseisenlem4  22823  qrng0  23002  qrngneg  23004  subrgchr  26406  nn0archi  26455  rezh  26544  qqhcn  26564  qqhucn  26565  fsumcnsrcl  29670  cnsrplycl  29671  rngunsnply  29677  zringsubgval  31012
  Copyright terms: Public domain W3C validator