Theorem subrgsubg 20835

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 20834	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20470	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2760	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20830	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2760	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20832	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20470	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19342	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1362	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  ‘cfv 6539  (class class class)co 7421  Basecbs 17393   ↾_s cress 17414  Grpcgrp 19150  SubGrpcsubg 19336  Ringcrg 20465  SubRingcsubrg 20827

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fv 6547  df-ov 7424  df-subg 19339  df-ring 20467  df-subrg 20828

This theorem is used by:  subrg0  20837  subrgbas  20839  subrgacl  20841  issubrg2  20850  subrgint  20853  resrhm  20859  resrhm2b  20860  rhmima  20862  subdrgint  21066  primefld0cl  21069  abvres  21094  zsssubrg  21737  gzrngunitlem  21744  zringlpirlem1  21774  zringcyg  21781  zringsubgval  21782  prmirred  21786  zndvds  21861  resubgval  21921  rzgrp  21935  issubassa2  22206  resspsrmul  22289  subrgpsr  22291  mplbas2  22357  gsumply1subr  22557  subrgnrg  24998  sranlm  25009  clmsub  25407  clmneg  25408  clmabs  25410  clmsubcl  25413  isncvsngp  25476  cphsqrtcl3  25514  tcphcph  25564  plypf1  26537  dvply2g  26612  taylply2  26701  circgrp  26886  circsubm  26887  jensenlem2  27321  amgmlem  27323  lgseisenlem4  27711  qrng0  27954  qrngneg  27956  subrgchr  33844  elrgspnlem4  33853  elrgspnsubrunlem2  33856  subrdom  33893  1fldgenq  33931  nn0archi  33955  idlinsubrg  34028  ressply1evls1  34144  ressply10g  34146  ressply1invg  34148  ressply1sub  34149  evls1subd  34151  vr1nz  34172  drgext0gsca  34271  fedgmullem1  34308  fedgmullem2  34309  evls1fldgencl  34349  fldextrspunlsplem  34352  fldextrspunlsp  34353  irngss  34366  extdgfialglem1  34371  extdgfialglem2  34372  algextdeglem1  34396  algextdeglem2  34397  algextdeglem3  34398  algextdeglem4  34399  algextdeglem5  34400  rtelextdg2lem  34405  constrelextdg2  34426  2sqr3minply  34459  rezh  34648  qqhcn  34670  qqhucn  34671  fsumcnsrcl  44262  cnsrplycl  44263  rngunsnply  44265  amgmwlem  51156