Theorem subrgsubg 20739

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 20738	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20377	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2760	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20734	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2760	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20736	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20377	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19249	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1362	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  ‘cfv 6533  (class class class)co 7413  Basecbs 17301   ↾_s cress 17322  Grpcgrp 19057  SubGrpcsubg 19243  Ringcrg 20372  SubRingcsubrg 20731

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7416  df-subg 19246  df-ring 20374  df-subrg 20732

This theorem is used by:  subrg0  20741  subrgbas  20743  subrgacl  20745  issubrg2  20754  subrgint  20757  resrhm  20763  resrhm2b  20764  rhmima  20766  subdrgint  20969  primefld0cl  20972  abvres  20997  zsssubrg  21638  gzrngunitlem  21645  zringlpirlem1  21675  zringcyg  21682  zringsubgval  21683  prmirred  21687  zndvds  21762  resubgval  21822  rzgrp  21836  issubassa2  22107  resspsrmul  22190  subrgpsr  22192  mplbas2  22258  gsumply1subr  22458  subrgnrg  24899  sranlm  24910  clmsub  25308  clmneg  25309  clmabs  25311  clmsubcl  25314  isncvsngp  25377  cphsqrtcl3  25415  tcphcph  25465  plypf1  26438  dvply2g  26515  taylply2  26604  circgrp  26789  circsubm  26790  jensenlem2  27224  amgmlem  27226  lgseisenlem4  27614  qrng0  27857  qrngneg  27859  subrgchr  33676  elrgspnlem4  33685  elrgspnsubrunlem2  33688  subrdom  33725  1fldgenq  33763  nn0archi  33787  idlinsubrg  33859  ressply1evls1  33975  ressply10g  33977  ressply1invg  33979  ressply1sub  33980  evls1subd  33982  vr1nz  34003  drgext0gsca  34102  fedgmullem1  34139  fedgmullem2  34140  evls1fldgencl  34180  fldextrspunlsplem  34183  fldextrspunlsp  34184  irngss  34197  extdgfialglem1  34202  extdgfialglem2  34203  algextdeglem1  34227  algextdeglem2  34228  algextdeglem3  34229  algextdeglem4  34230  algextdeglem5  34231  rtelextdg2lem  34236  constrelextdg2  34257  2sqr3minply  34290  rezh  34479  qqhcn  34501  qqhucn  34502  fsumcnsrcl  44007  cnsrplycl  44008  rngunsnply  44010  amgmwlem  50820