Theorem subrgsubg 20510

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 20509	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20173	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2736	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20505	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2736	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20507	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20173	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19056	. 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp))
11	3, 5, 9, 10	syl3anbrc 1344	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  ‘cfv 6492  (class class class)co 7358  Basecbs 17136   ↾_s cress 17157  Grpcgrp 18863  SubGrpcsubg 19050  Ringcrg 20168  SubRingcsubrg 20502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-subg 19053  df-ring 20170  df-subrg 20503

This theorem is referenced by:  subrg0  20512  subrgbas  20514  subrgacl  20516  issubrg2  20525  subrgint  20528  resrhm  20534  resrhm2b  20535  rhmima  20537  subdrgint  20736  primefld0cl  20739  abvres  20764  zsssubrg  21380  gzrngunitlem  21387  zringlpirlem1  21417  zringcyg  21424  zringsubgval  21425  prmirred  21429  zndvds  21504  resubgval  21564  rzgrp  21578  issubassa2  21848  resspsrmul  21931  subrgpsr  21933  mplbas2  21997  gsumply1subr  22174  subrgnrg  24617  sranlm  24628  clmsub  25036  clmneg  25037  clmabs  25039  clmsubcl  25042  isncvsngp  25105  cphsqrtcl3  25143  tcphcph  25193  plypf1  26173  dvply2g  26248  dvply2gOLD  26249  taylply2  26331  taylply2OLD  26332  circgrp  26517  circsubm  26518  jensenlem2  26954  amgmlem  26956  lgseisenlem4  27345  qrng0  27588  qrngneg  27590  subrgchr  33319  elrgspnlem4  33327  elrgspnsubrunlem2  33330  subrdom  33367  1fldgenq  33404  nn0archi  33428  idlinsubrg  33512  ressply1evls1  33646  ressply10g  33648  ressply1invg  33650  ressply1sub  33651  evls1subd  33653  vr1nz  33674  drgext0gsca  33748  fedgmullem1  33786  fedgmullem2  33787  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  irngss  33844  extdgfialglem1  33849  extdgfialglem2  33850  algextdeglem1  33874  algextdeglem2  33875  algextdeglem3  33876  algextdeglem4  33877  algextdeglem5  33878  rtelextdg2lem  33883  constrelextdg2  33904  2sqr3minply  33937  rezh  34126  qqhcn  34148  qqhucn  34149  fsumcnsrcl  43408  cnsrplycl  43409  rngunsnply  43411  amgmwlem  50047