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

Theorem subrgsubg 17647
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 17646 . . 3  |-  ( A  e.  (SubRing `  R
)  ->  R  e.  Ring )
2 ringgrp 17415 . . 3  |-  ( R  e.  Ring  ->  R  e. 
Grp )
31, 2syl 17 . 2  |-  ( A  e.  (SubRing `  R
)  ->  R  e.  Grp )
4 eqid 2402 . . 3  |-  ( Base `  R )  =  (
Base `  R )
54subrgss 17642 . 2  |-  ( A  e.  (SubRing `  R
)  ->  A  C_  ( Base `  R ) )
6 eqid 2402 . . . 4  |-  ( Rs  A )  =  ( Rs  A )
76subrgring 17644 . . 3  |-  ( A  e.  (SubRing `  R
)  ->  ( Rs  A
)  e.  Ring )
8 ringgrp 17415 . . 3  |-  ( ( Rs  A )  e.  Ring  -> 
( Rs  A )  e.  Grp )
97, 8syl 17 . 2  |-  ( A  e.  (SubRing `  R
)  ->  ( Rs  A
)  e.  Grp )
104issubg 16417 . 2  |-  ( A  e.  (SubGrp `  R
)  <->  ( R  e. 
Grp  /\  A  C_  ( Base `  R )  /\  ( Rs  A )  e.  Grp ) )
113, 5, 9, 10syl3anbrc 1181 1  |-  ( A  e.  (SubRing `  R
)  ->  A  e.  (SubGrp `  R ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842    C_ wss 3413   ` cfv 5525  (class class class)co 6234   Basecbs 14733   ↾s cress 14734   Grpcgrp 16269  SubGrpcsubg 16411   Ringcrg 17410  SubRingcsubrg 17637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fv 5533  df-ov 6237  df-subg 16414  df-ring 17412  df-subrg 17639
This theorem is referenced by:  subrg0  17648  subrgbas  17650  subrgacl  17652  issubrg2  17661  subrgint  17663  resrhm  17670  rhmima  17672  abvres  17700  issubassa2  18206  resspsrmul  18284  subrgpsr  18286  mplbas2  18346  mplbas2OLD  18347  gsumply1subr  18487  zsssubrg  18688  gzrngunitlem  18694  zringlpirlem1  18714  zringcyg  18718  prmirred  18724  zndvds  18778  resubgval  18835  subrgnrg  21366  sranlm  21377  clmsub  21764  clmneg  21765  clmabs  21766  clmsubcl  21769  cphsqrtcl3  21818  tchcph  21864  plypf1  22793  dvply2g  22865  taylply2  22947  circgrp  23123  circsubm  23124  rzgrp  23125  jensenlem2  23535  amgmlem  23537  lgseisenlem4  23900  qrng0  24079  qrngneg  24081  subrgchr  28117  nn0archi  28166  rezh  28284  qqhcn  28304  qqhucn  28305  fsumcnsrcl  35460  cnsrplycl  35461  rngunsnply  35467  zringsubgval  38486
  Copyright terms: Public domain W3C validator