Theorem subrgsubg 19101

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 19100	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 18865	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2798	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 19096	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2798	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 19098	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 18865	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 17904	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1444	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2157   ⊆ wss 3768  ‘cfv 6100  (class class class)co 6877  Basecbs 16181   ↾_s cress 16182  Grpcgrp 17735  SubGrpcsubg 17898  Ringcrg 18860  SubRingcsubrg 19091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3386  df-sbc 3633  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4628  df-br 4843  df-opab 4905  df-mpt 4922  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6063  df-fun 6102  df-fv 6108  df-ov 6880  df-subg 17901  df-ring 18862  df-subrg 19093

This theorem is referenced by:  subrg0  19102  subrgbas  19104  subrgacl  19106  issubrg2  19115  subrgint  19117  resrhm  19124  rhmima  19126  abvres  19154  issubassa2  19665  resspsrmul  19737  subrgpsr  19739  mplbas2  19790  gsumply1subr  19923  zsssubrg  20123  gzrngunitlem  20130  zringlpirlem1  20151  zringcyg  20158  prmirred  20162  zndvds  20216  resubgval  20275  rzgrp  20289  subrgnrg  22802  sranlm  22813  clmsub  23204  clmneg  23205  clmabs  23207  clmsubcl  23210  isncvsngp  23273  cphsqrtcl3  23311  tcphcph  23360  plypf1  24306  dvply2g  24378  taylply2  24460  circgrp  24637  circsubm  24638  jensenlem2  25063  amgmlem  25065  lgseisenlem4  25452  qrng0  25659  qrngneg  25661  subrgchr  30303  nn0archi  30352  rezh  30524  qqhcn  30544  qqhucn  30545  fsumcnsrcl  38510  cnsrplycl  38511  rngunsnply  38517  zringsubgval  42971  amgmwlem  43339