Theorem subrgsubg 20134

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 20133	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 19882	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2737	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20129	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2737	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20131	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 19882	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 18851	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1343	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3901  ‘cfv 6483  (class class class)co 7341  Basecbs 17009   ↾_s cress 17038  Grpcgrp 18673  SubGrpcsubg 18845  Ringcrg 19877  SubRingcsubrg 20124

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 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3731  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-mpt 5180  df-id 5522  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6435  df-fun 6485  df-fv 6491  df-ov 7344  df-subg 18848  df-ring 19879  df-subrg 20126

This theorem is referenced by:  subrg0  20135  subrgbas  20137  subrgacl  20139  issubrg2  20148  subrgint  20150  resrhm  20157  rhmima  20159  subdrgint  20176  primefld0cl  20179  abvres  20204  zsssubrg  20761  gzrngunitlem  20768  zringlpirlem1  20789  zringcyg  20796  zringsubgval  20797  prmirred  20801  zndvds  20862  resubgval  20919  rzgrp  20933  issubassa2  21201  resspsrmul  21291  subrgpsr  21293  mplbas2  21348  gsumply1subr  21510  subrgnrg  23942  sranlm  23953  clmsub  24348  clmneg  24349  clmabs  24351  clmsubcl  24354  isncvsngp  24418  cphsqrtcl3  24456  tcphcph  24506  plypf1  25478  dvply2g  25550  taylply2  25632  circgrp  25813  circsubm  25814  jensenlem2  26242  amgmlem  26244  lgseisenlem4  26631  qrng0  26874  qrngneg  26876  subrgchr  31776  1fldgenq  31791  nn0archi  31841  idlinsubrg  31903  drgext0gsca  31975  fedgmullem1  32006  fedgmullem2  32007  rezh  32217  qqhcn  32237  qqhucn  32238  selvval2lem4  40533  fsumcnsrcl  41305  cnsrplycl  41306  rngunsnply  41312  amgmwlem  46924