Theorem subrgsubg 20593

Description: A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)

Assertion

Ref	Expression
subrgsubg	⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Proof of Theorem subrgsubg

Step	Hyp	Ref	Expression
1		subrgrcl 20592	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20255	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2734	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20588	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2734	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20590	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20255	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19156	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1342	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  ‘cfv 6562  (class class class)co 7430  Basecbs 17244   ↾_s cress 17273  Grpcgrp 18963  SubGrpcsubg 19150  Ringcrg 20250  SubRingcsubrg 20585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-subg 19153  df-ring 20252  df-subrg 20586

This theorem is referenced by:  subrg0  20595  subrgbas  20597  subrgacl  20599  issubrg2  20608  subrgint  20611  resrhm  20617  resrhm2b  20618  rhmima  20620  subdrgint  20820  primefld0cl  20823  abvres  20848  zsssubrg  21460  gzrngunitlem  21467  zringlpirlem1  21490  zringcyg  21497  zringsubgval  21498  prmirred  21502  zndvds  21585  resubgval  21644  rzgrp  21658  issubassa2  21929  resspsrmul  22013  subrgpsr  22015  mplbas2  22077  gsumply1subr  22250  subrgnrg  24709  sranlm  24720  clmsub  25126  clmneg  25127  clmabs  25129  clmsubcl  25132  isncvsngp  25196  cphsqrtcl3  25234  tcphcph  25284  plypf1  26265  dvply2g  26340  dvply2gOLD  26341  taylply2  26423  taylply2OLD  26424  circgrp  26608  circsubm  26609  jensenlem2  27045  amgmlem  27047  lgseisenlem4  27436  qrng0  27679  qrngneg  27681  subrgchr  33226  elrgspnlem4  33234  subrdom  33268  1fldgenq  33303  nn0archi  33354  idlinsubrg  33438  ressply10g  33571  ressply1invg  33573  ressply1sub  33574  evls1subd  33576  drgext0gsca  33620  fedgmullem1  33656  fedgmullem2  33657  evls1fldgencl  33694  irngss  33701  algextdeglem1  33722  algextdeglem2  33723  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  rtelextdg2lem  33731  constrelextdg2  33751  2sqr3minply  33752  rezh  33931  qqhcn  33953  qqhucn  33954  fsumcnsrcl  43154  cnsrplycl  43155  rngunsnply  43157  amgmwlem  49032