Theorem subrgsubg 20549

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 20548	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20210	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2739	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20544	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2739	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20546	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20210	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19093	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1350	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883  ‘cfv 6485  (class class class)co 7356  Basecbs 17170   ↾_s cress 17191  Grpcgrp 18900  SubGrpcsubg 19087  Ringcrg 20205  SubRingcsubrg 20541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fv 6493  df-ov 7359  df-subg 19090  df-ring 20207  df-subrg 20542

This theorem is referenced by:  subrg0  20551  subrgbas  20553  subrgacl  20555  issubrg2  20564  subrgint  20567  resrhm  20573  resrhm2b  20574  rhmima  20576  subdrgint  20775  primefld0cl  20778  abvres  20803  zsssubrg  21400  gzrngunitlem  21407  zringlpirlem1  21437  zringcyg  21444  zringsubgval  21445  prmirred  21449  zndvds  21524  resubgval  21584  rzgrp  21598  issubassa2  21867  resspsrmul  21950  subrgpsr  21952  mplbas2  22018  gsumply1subr  22218  subrgnrg  24656  sranlm  24667  clmsub  25065  clmneg  25066  clmabs  25068  clmsubcl  25071  isncvsngp  25134  cphsqrtcl3  25172  tcphcph  25222  plypf1  26195  dvply2g  26269  taylply2  26351  circgrp  26534  circsubm  26535  jensenlem2  26969  amgmlem  26971  lgseisenlem4  27359  qrng0  27602  qrngneg  27604  subrgchr  33318  elrgspnlem4  33326  elrgspnsubrunlem2  33329  subrdom  33366  1fldgenq  33406  nn0archi  33430  idlinsubrg  33514  ressply1evls1  33648  ressply10g  33650  ressply1invg  33652  ressply1sub  33653  evls1subd  33655  vr1nz  33676  drgext0gsca  33776  fedgmullem1  33813  fedgmullem2  33814  evls1fldgencl  33854  fldextrspunlsplem  33857  fldextrspunlsp  33858  irngss  33871  extdgfialglem1  33876  extdgfialglem2  33877  algextdeglem1  33901  algextdeglem2  33902  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  rtelextdg2lem  33910  constrelextdg2  33931  2sqr3minply  33964  rezh  34153  qqhcn  34175  qqhucn  34176  fsumcnsrcl  43611  cnsrplycl  43612  rngunsnply  43614  amgmwlem  50292