Theorem subrgsubg 19544

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 19543	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 19305	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2824	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 19539	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2824	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 19541	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 19305	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 18282	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1339	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3939  ‘cfv 6358  (class class class)co 7159  Basecbs 16486   ↾_s cress 16487  Grpcgrp 18106  SubGrpcsubg 18276  Ringcrg 19300  SubRingcsubrg 19534

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fv 6366  df-ov 7162  df-subg 18279  df-ring 19302  df-subrg 19536

This theorem is referenced by:  subrg0  19545  subrgbas  19547  subrgacl  19549  issubrg2  19558  subrgint  19560  resrhm  19567  rhmima  19569  subdrgint  19585  primefld0cl  19588  abvres  19613  issubassa2  20124  resspsrmul  20200  subrgpsr  20202  mplbas2  20254  gsumply1subr  20405  zsssubrg  20606  gzrngunitlem  20613  zringlpirlem1  20634  zringcyg  20641  prmirred  20645  zndvds  20699  resubgval  20756  rzgrp  20770  subrgnrg  23285  sranlm  23296  clmsub  23687  clmneg  23688  clmabs  23690  clmsubcl  23693  isncvsngp  23756  cphsqrtcl3  23794  tcphcph  23843  plypf1  24805  dvply2g  24877  taylply2  24959  circgrp  25139  circsubm  25140  jensenlem2  25568  amgmlem  25570  lgseisenlem4  25957  qrng0  26200  qrngneg  26202  subrgchr  30869  nn0archi  30920  drgext0gsca  30998  fedgmullem1  31029  fedgmullem2  31030  rezh  31216  qqhcn  31236  qqhucn  31237  selvval2lem4  39142  fsumcnsrcl  39772  cnsrplycl  39773  rngunsnply  39779  zringsubgval  44456  amgmwlem  44910