Theorem subrgsubg 20664

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 20663	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20322	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2769	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20659	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2769	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20661	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20322	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19194	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1360	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913  ‘cfv 6539  (class class class)co 7413  Basecbs 17271   ↾_s cress 17292  Grpcgrp 19002  SubGrpcsubg 19188  Ringcrg 20317  SubRingcsubrg 20656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-iota 6495  df-fun 6541  df-fv 6547  df-ov 7416  df-subg 19191  df-ring 20319  df-subrg 20657

This theorem is referenced by:  subrg0  20666  subrgbas  20668  subrgacl  20670  issubrg2  20679  subrgint  20682  resrhm  20688  resrhm2b  20689  rhmima  20691  subdrgint  20886  primefld0cl  20889  abvres  20914  zsssubrg  21546  gzrngunitlem  21553  zringlpirlem1  21583  zringcyg  21590  zringsubgval  21591  prmirred  21595  zndvds  21670  resubgval  21730  rzgrp  21744  issubassa2  22013  resspsrmul  22096  subrgpsr  22098  mplbas2  22164  gsumply1subr  22364  subrgnrg  24801  sranlm  24812  clmsub  25210  clmneg  25211  clmabs  25213  clmsubcl  25216  isncvsngp  25279  cphsqrtcl3  25317  tcphcph  25367  plypf1  26340  dvply2g  26417  taylply2  26499  circgrp  26685  circsubm  26686  jensenlem2  27120  amgmlem  27122  lgseisenlem4  27510  qrng0  27753  qrngneg  27755  subrgchr  33499  elrgspnlem4  33508  elrgspnsubrunlem2  33511  subrdom  33548  1fldgenq  33588  nn0archi  33612  idlinsubrg  33685  ressply1evls1  33802  ressply10g  33804  ressply1invg  33806  ressply1sub  33807  evls1subd  33809  vr1nz  33830  drgext0gsca  33929  fedgmullem1  33966  fedgmullem2  33967  evls1fldgencl  34007  fldextrspunlsplem  34010  fldextrspunlsp  34011  irngss  34024  extdgfialglem1  34029  extdgfialglem2  34030  algextdeglem1  34054  algextdeglem2  34055  algextdeglem3  34056  algextdeglem4  34057  algextdeglem5  34058  rtelextdg2lem  34063  constrelextdg2  34084  2sqr3minply  34117  rezh  34306  qqhcn  34328  qqhucn  34329  fsumcnsrcl  43822  cnsrplycl  43823  rngunsnply  43825  amgmwlem  50513