Theorem subrgsubg 20493

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 20492	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20157	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2731	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20488	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2731	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20490	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20157	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19039	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1344	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3902  ‘cfv 6481  (class class class)co 7346  Basecbs 17120   ↾_s cress 17141  Grpcgrp 18846  SubGrpcsubg 19033  Ringcrg 20152  SubRingcsubrg 20485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-subg 19036  df-ring 20154  df-subrg 20486

This theorem is referenced by:  subrg0  20495  subrgbas  20497  subrgacl  20499  issubrg2  20508  subrgint  20511  resrhm  20517  resrhm2b  20518  rhmima  20520  subdrgint  20719  primefld0cl  20722  abvres  20747  zsssubrg  21363  gzrngunitlem  21370  zringlpirlem1  21400  zringcyg  21407  zringsubgval  21408  prmirred  21412  zndvds  21487  resubgval  21547  rzgrp  21561  issubassa2  21830  resspsrmul  21914  subrgpsr  21916  mplbas2  21978  gsumply1subr  22147  subrgnrg  24589  sranlm  24600  clmsub  25008  clmneg  25009  clmabs  25011  clmsubcl  25014  isncvsngp  25077  cphsqrtcl3  25115  tcphcph  25165  plypf1  26145  dvply2g  26220  dvply2gOLD  26221  taylply2  26303  taylply2OLD  26304  circgrp  26489  circsubm  26490  jensenlem2  26926  amgmlem  26928  lgseisenlem4  27317  qrng0  27560  qrngneg  27562  subrgchr  33202  elrgspnlem4  33210  elrgspnsubrunlem2  33213  subrdom  33249  1fldgenq  33286  nn0archi  33310  idlinsubrg  33394  ressply1evls1  33526  ressply10g  33528  ressply1invg  33530  ressply1sub  33531  evls1subd  33533  vr1nz  33552  drgext0gsca  33602  fedgmullem1  33640  fedgmullem2  33641  evls1fldgencl  33681  fldextrspunlsplem  33684  fldextrspunlsp  33685  irngss  33698  extdgfialglem1  33703  extdgfialglem2  33704  algextdeglem1  33728  algextdeglem2  33729  algextdeglem3  33730  algextdeglem4  33731  algextdeglem5  33732  rtelextdg2lem  33737  constrelextdg2  33758  2sqr3minply  33791  rezh  33980  qqhcn  34002  qqhucn  34003  fsumcnsrcl  43205  cnsrplycl  43206  rngunsnply  43208  amgmwlem  49840