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

Theorem subrgsubg 15567
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 15566 . . 3  |-  ( A  e.  (SubRing `  R
)  ->  R  e.  Ring )
2 rnggrp 15362 . . 3  |-  ( R  e.  Ring  ->  R  e. 
Grp )
31, 2syl 15 . 2  |-  ( A  e.  (SubRing `  R
)  ->  R  e.  Grp )
4 eqid 2296 . . 3  |-  ( Base `  R )  =  (
Base `  R )
54subrgss 15562 . 2  |-  ( A  e.  (SubRing `  R
)  ->  A  C_  ( Base `  R ) )
6 eqid 2296 . . . 4  |-  ( Rs  A )  =  ( Rs  A )
76subrgrng 15564 . . 3  |-  ( A  e.  (SubRing `  R
)  ->  ( Rs  A
)  e.  Ring )
8 rnggrp 15362 . . 3  |-  ( ( Rs  A )  e.  Ring  -> 
( Rs  A )  e.  Grp )
97, 8syl 15 . 2  |-  ( A  e.  (SubRing `  R
)  ->  ( Rs  A
)  e.  Grp )
104issubg 14637 . 2  |-  ( A  e.  (SubGrp `  R
)  <->  ( R  e. 
Grp  /\  A  C_  ( Base `  R )  /\  ( Rs  A )  e.  Grp ) )
113, 5, 9, 10syl3anbrc 1136 1  |-  ( A  e.  (SubRing `  R
)  ->  A  e.  (SubGrp `  R ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165   ` cfv 5271  (class class class)co 5874   Basecbs 13164   ↾s cress 13165   Grpcgrp 14378  SubGrpcsubg 14631   Ringcrg 15353  SubRingcsubrg 15557
This theorem is referenced by:  subrg0  15568  subrgbas  15570  subrgacl  15572  issubrg2  15581  subrgint  15583  resrhm  15590  rhmima  15592  abvres  15620  issubassa2  16100  resspsrmul  16177  subrgpsr  16179  mplbas2  16228  zsssubrg  16446  gzrngunitlem  16452  zlpirlem1  16457  zcyg  16461  prmirred  16464  expghm  16466  mulgrhm2  16477  zndvds  16519  frgpcyg  16543  subrgnrg  18200  sranlm  18211  clmsub  18594  clmneg  18595  clmabs  18596  clmsubcl  18599  cphsqrcl3  18639  tchcph  18683  plypf1  19610  dvply2g  19681  taylply2  19763  jensenlem2  20298  amgmlem  20300  lgseisenlem4  20607  dchrisum0flblem1  20673  qrng0  20786  qrngneg  20788  fsumcnsrcl  27474  cnsrplycl  27475  rngunsnply  27481
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fv 5279  df-ov 5877  df-subg 14634  df-rng 15356  df-subrg 15559
  Copyright terms: Public domain W3C validator