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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  ‘cfv 6514  (class class class)co 7390  Basecbs 17186   ↾_s cress 17207  Grpcgrp 18872  SubGrpcsubg 19059  Ringcrg 20149  SubRingcsubrg 20485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-subg 19062  df-ring 20151  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  21349  gzrngunitlem  21356  zringlpirlem1  21379  zringcyg  21386  zringsubgval  21387  prmirred  21391  zndvds  21466  resubgval  21525  rzgrp  21539  issubassa2  21808  resspsrmul  21892  subrgpsr  21894  mplbas2  21956  gsumply1subr  22125  subrgnrg  24568  sranlm  24579  clmsub  24987  clmneg  24988  clmabs  24990  clmsubcl  24993  isncvsngp  25056  cphsqrtcl3  25094  tcphcph  25144  plypf1  26124  dvply2g  26199  dvply2gOLD  26200  taylply2  26282  taylply2OLD  26283  circgrp  26468  circsubm  26469  jensenlem2  26905  amgmlem  26907  lgseisenlem4  27296  qrng0  27539  qrngneg  27541  subrgchr  33195  elrgspnlem4  33203  elrgspnsubrunlem2  33206  subrdom  33242  1fldgenq  33279  nn0archi  33325  idlinsubrg  33409  ressply1evls1  33541  ressply10g  33543  ressply1invg  33545  ressply1sub  33546  evls1subd  33548  vr1nz  33566  drgext0gsca  33594  fedgmullem1  33632  fedgmullem2  33633  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  irngss  33689  algextdeglem1  33714  algextdeglem2  33715  algextdeglem3  33716  algextdeglem4  33717  algextdeglem5  33718  rtelextdg2lem  33723  constrelextdg2  33744  2sqr3minply  33777  rezh  33966  qqhcn  33988  qqhucn  33989  fsumcnsrcl  43162  cnsrplycl  43163  rngunsnply  43165  amgmwlem  49795