Theorem subrgsubg 20516

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 20515	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20178	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2728	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20511	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2728	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20513	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20178	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19081	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1341	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3947  ‘cfv 6548  (class class class)co 7420  Basecbs 17180   ↾_s cress 17209  Grpcgrp 18890  SubGrpcsubg 19075  Ringcrg 20173  SubRingcsubrg 20506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fv 6556  df-ov 7423  df-subg 19078  df-ring 20175  df-subrg 20508

This theorem is referenced by:  subrg0  20518  subrgbas  20520  subrgacl  20522  issubrg2  20531  subrgint  20534  resrhm  20540  resrhm2b  20541  rhmima  20543  subdrgint  20691  primefld0cl  20694  abvres  20719  zsssubrg  21358  gzrngunitlem  21365  zringlpirlem1  21388  zringcyg  21395  zringsubgval  21396  prmirred  21400  zndvds  21483  resubgval  21541  rzgrp  21555  issubassa2  21825  resspsrmul  21919  subrgpsr  21921  mplbas2  21980  gsumply1subr  22152  subrgnrg  24603  sranlm  24614  clmsub  25020  clmneg  25021  clmabs  25023  clmsubcl  25026  isncvsngp  25090  cphsqrtcl3  25128  tcphcph  25178  plypf1  26159  dvply2g  26232  dvply2gOLD  26233  taylply2  26315  taylply2OLD  26316  circgrp  26499  circsubm  26500  jensenlem2  26933  amgmlem  26935  lgseisenlem4  27324  qrng0  27567  qrngneg  27569  subrgchr  32958  1fldgenq  33022  nn0archi  33072  idlinsubrg  33160  ressply10g  33252  ressply1invg  33254  ressply1sub  33255  evls1subd  33256  drgext0gsca  33291  fedgmullem1  33327  fedgmullem2  33328  evls1fldgencl  33358  irngss  33365  algextdeglem1  33385  algextdeglem2  33386  algextdeglem3  33387  algextdeglem4  33388  algextdeglem5  33389  rezh  33572  qqhcn  33592  qqhucn  33593  fsumcnsrcl  42590  cnsrplycl  42591  rngunsnply  42597  amgmwlem  48235