Theorem subrgsubg 20561

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 20560	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20221	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2726	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20556	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2726	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20558	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20221	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19120	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1340	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3947  ‘cfv 6554  (class class class)co 7424  Basecbs 17213   ↾_s cress 17242  Grpcgrp 18928  SubGrpcsubg 19114  Ringcrg 20216  SubRingcsubrg 20551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fv 6562  df-ov 7427  df-subg 19117  df-ring 20218  df-subrg 20553

This theorem is referenced by:  subrg0  20563  subrgbas  20565  subrgacl  20567  issubrg2  20576  subrgint  20579  resrhm  20585  resrhm2b  20586  rhmima  20588  subdrgint  20782  primefld0cl  20785  abvres  20810  zsssubrg  21422  gzrngunitlem  21429  zringlpirlem1  21452  zringcyg  21459  zringsubgval  21460  prmirred  21464  zndvds  21547  resubgval  21605  rzgrp  21619  issubassa2  21889  resspsrmul  21985  subrgpsr  21987  mplbas2  22049  gsumply1subr  22223  subrgnrg  24681  sranlm  24692  clmsub  25098  clmneg  25099  clmabs  25101  clmsubcl  25104  isncvsngp  25168  cphsqrtcl3  25206  tcphcph  25256  plypf1  26239  dvply2g  26312  dvply2gOLD  26313  taylply2  26395  taylply2OLD  26396  circgrp  26579  circsubm  26580  jensenlem2  27016  amgmlem  27018  lgseisenlem4  27407  qrng0  27650  qrngneg  27652  subrgchr  33102  subrdom  33137  1fldgenq  33172  nn0archi  33222  idlinsubrg  33306  ressply10g  33439  ressply1invg  33441  ressply1sub  33442  evls1subd  33444  drgext0gsca  33488  fedgmullem1  33524  fedgmullem2  33525  evls1fldgencl  33556  irngss  33563  algextdeglem1  33584  algextdeglem2  33585  algextdeglem3  33586  algextdeglem4  33587  algextdeglem5  33588  rtelextdg2lem  33604  2sqr3minply  33607  rezh  33786  qqhcn  33806  qqhucn  33807  fsumcnsrcl  42827  cnsrplycl  42828  rngunsnply  42834  amgmwlem  48550