Theorem subrgsubg 20663

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3906  ‘cfv 6538  (class class class)co 7412  Basecbs 17270   ↾_s cress 17291  Grpcgrp 19001  SubGrpcsubg 19187  Ringcrg 20316  SubRingcsubrg 20655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-subg 19190  df-ring 20318  df-subrg 20656

This theorem is referenced by:  subrg0  20665  subrgbas  20667  subrgacl  20669  issubrg2  20678  subrgint  20681  resrhm  20687  resrhm2b  20688  rhmima  20690  subdrgint  20887  primefld0cl  20890  abvres  20915  zsssubrg  21556  gzrngunitlem  21563  zringlpirlem1  21593  zringcyg  21600  zringsubgval  21601  prmirred  21605  zndvds  21680  resubgval  21740  rzgrp  21754  issubassa2  22023  resspsrmul  22106  subrgpsr  22108  mplbas2  22174  gsumply1subr  22374  subrgnrg  24811  sranlm  24822  clmsub  25220  clmneg  25221  clmabs  25223  clmsubcl  25226  isncvsngp  25289  cphsqrtcl3  25327  tcphcph  25377  plypf1  26350  dvply2g  26427  taylply2  26512  circgrp  26698  circsubm  26699  jensenlem2  27133  amgmlem  27135  lgseisenlem4  27523  qrng0  27766  qrngneg  27768  subrgchr  33537  elrgspnlem4  33546  elrgspnsubrunlem2  33549  subrdom  33586  1fldgenq  33624  nn0archi  33648  idlinsubrg  33720  ressply1evls1  33836  ressply10g  33838  ressply1invg  33840  ressply1sub  33841  evls1subd  33843  vr1nz  33864  drgext0gsca  33963  fedgmullem1  34000  fedgmullem2  34001  evls1fldgencl  34041  fldextrspunlsplem  34044  fldextrspunlsp  34045  irngss  34058  extdgfialglem1  34063  extdgfialglem2  34064  algextdeglem1  34088  algextdeglem2  34089  algextdeglem3  34090  algextdeglem4  34091  algextdeglem5  34092  rtelextdg2lem  34097  constrelextdg2  34118  2sqr3minply  34151  rezh  34340  qqhcn  34362  qqhucn  34363  fsumcnsrcl  43876  cnsrplycl  43877  rngunsnply  43879  amgmwlem  50585