Theorem subrgsubg 20554

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 20553	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20219	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2736	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20549	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2736	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20551	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20219	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19102	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1345	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  ‘cfv 6498  (class class class)co 7367  Basecbs 17179   ↾_s cress 17200  Grpcgrp 18909  SubGrpcsubg 19096  Ringcrg 20214  SubRingcsubrg 20546

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-subg 19099  df-ring 20216  df-subrg 20547

This theorem is referenced by:  subrg0  20556  subrgbas  20558  subrgacl  20560  issubrg2  20569  subrgint  20572  resrhm  20578  resrhm2b  20579  rhmima  20581  subdrgint  20780  primefld0cl  20783  abvres  20808  zsssubrg  21405  gzrngunitlem  21412  zringlpirlem1  21442  zringcyg  21449  zringsubgval  21450  prmirred  21454  zndvds  21529  resubgval  21589  rzgrp  21603  issubassa2  21872  resspsrmul  21954  subrgpsr  21956  mplbas2  22020  gsumply1subr  22197  subrgnrg  24638  sranlm  24649  clmsub  25047  clmneg  25048  clmabs  25050  clmsubcl  25053  isncvsngp  25116  cphsqrtcl3  25154  tcphcph  25204  plypf1  26177  dvply2g  26251  taylply2  26333  circgrp  26516  circsubm  26517  jensenlem2  26951  amgmlem  26953  lgseisenlem4  27341  qrng0  27584  qrngneg  27586  subrgchr  33298  elrgspnlem4  33306  elrgspnsubrunlem2  33309  subrdom  33346  1fldgenq  33383  nn0archi  33407  idlinsubrg  33491  ressply1evls1  33625  ressply10g  33627  ressply1invg  33629  ressply1sub  33630  evls1subd  33632  vr1nz  33653  drgext0gsca  33736  fedgmullem1  33773  fedgmullem2  33774  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  irngss  33831  extdgfialglem1  33836  extdgfialglem2  33837  algextdeglem1  33861  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  rtelextdg2lem  33870  constrelextdg2  33891  2sqr3minply  33924  rezh  34113  qqhcn  34135  qqhucn  34136  fsumcnsrcl  43594  cnsrplycl  43595  rngunsnply  43597  amgmwlem  50277