Theorem subrgsubg 20614

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 20613	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20275	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2761	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20609	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2761	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20611	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20275	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19159	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1356	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3902  ‘cfv 6516  (class class class)co 7391  Basecbs 17236   ↾_s cress 17257  Grpcgrp 18966  SubGrpcsubg 19153  Ringcrg 20270  SubRingcsubrg 20606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fv 6524  df-ov 7394  df-subg 19156  df-ring 20272  df-subrg 20607

This theorem is referenced by:  subrg0  20616  subrgbas  20618  subrgacl  20620  issubrg2  20629  subrgint  20632  resrhm  20638  resrhm2b  20639  rhmima  20641  subdrgint  20840  primefld0cl  20843  abvres  20868  zsssubrg  21465  gzrngunitlem  21472  zringlpirlem1  21502  zringcyg  21509  zringsubgval  21510  prmirred  21514  zndvds  21589  resubgval  21649  rzgrp  21663  issubassa2  21932  resspsrmul  22015  subrgpsr  22017  mplbas2  22083  gsumply1subr  22283  subrgnrg  24721  sranlm  24732  clmsub  25130  clmneg  25131  clmabs  25133  clmsubcl  25136  isncvsngp  25199  cphsqrtcl3  25237  tcphcph  25287  plypf1  26260  dvply2g  26337  taylply2  26419  circgrp  26605  circsubm  26606  jensenlem2  27040  amgmlem  27042  lgseisenlem4  27430  qrng0  27673  qrngneg  27675  subrgchr  33378  elrgspnlem4  33387  elrgspnsubrunlem2  33390  subrdom  33430  1fldgenq  33470  nn0archi  33494  idlinsubrg  33578  ressply1evls1  33722  ressply10g  33724  ressply1invg  33726  ressply1sub  33727  evls1subd  33729  vr1nz  33750  drgext0gsca  33850  fedgmullem1  33887  fedgmullem2  33888  evls1fldgencl  33928  fldextrspunlsplem  33931  fldextrspunlsp  33932  irngss  33945  extdgfialglem1  33950  extdgfialglem2  33951  algextdeglem1  33975  algextdeglem2  33976  algextdeglem3  33977  algextdeglem4  33978  algextdeglem5  33979  rtelextdg2lem  33984  constrelextdg2  34005  2sqr3minply  34038  rezh  34227  qqhcn  34249  qqhucn  34250  fsumcnsrcl  43704  cnsrplycl  43705  rngunsnply  43707  amgmwlem  50384