Theorem subrgsubg 20522

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  ‘cfv 6500  (class class class)co 7368  Basecbs 17148   ↾_s cress 17169  Grpcgrp 18875  SubGrpcsubg 19062  Ringcrg 20180  SubRingcsubrg 20514

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 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-subg 19065  df-ring 20182  df-subrg 20515

This theorem is referenced by:  subrg0  20524  subrgbas  20526  subrgacl  20528  issubrg2  20537  subrgint  20540  resrhm  20546  resrhm2b  20547  rhmima  20549  subdrgint  20748  primefld0cl  20751  abvres  20776  zsssubrg  21392  gzrngunitlem  21399  zringlpirlem1  21429  zringcyg  21436  zringsubgval  21437  prmirred  21441  zndvds  21516  resubgval  21576  rzgrp  21590  issubassa2  21860  resspsrmul  21943  subrgpsr  21945  mplbas2  22009  gsumply1subr  22186  subrgnrg  24629  sranlm  24640  clmsub  25048  clmneg  25049  clmabs  25051  clmsubcl  25054  isncvsngp  25117  cphsqrtcl3  25155  tcphcph  25205  plypf1  26185  dvply2g  26260  dvply2gOLD  26261  taylply2  26343  taylply2OLD  26344  circgrp  26529  circsubm  26530  jensenlem2  26966  amgmlem  26968  lgseisenlem4  27357  qrng0  27600  qrngneg  27602  subrgchr  33330  elrgspnlem4  33338  elrgspnsubrunlem2  33341  subrdom  33378  1fldgenq  33415  nn0archi  33439  idlinsubrg  33523  ressply1evls1  33657  ressply10g  33659  ressply1invg  33661  ressply1sub  33662  evls1subd  33664  vr1nz  33685  drgext0gsca  33768  fedgmullem1  33806  fedgmullem2  33807  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  irngss  33864  extdgfialglem1  33869  extdgfialglem2  33870  algextdeglem1  33894  algextdeglem2  33895  algextdeglem3  33896  algextdeglem4  33897  algextdeglem5  33898  rtelextdg2lem  33903  constrelextdg2  33924  2sqr3minply  33957  rezh  34146  qqhcn  34168  qqhucn  34169  fsumcnsrcl  43520  cnsrplycl  43521  rngunsnply  43523  amgmwlem  50158