Theorem subrgsubg 20556

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3890  ‘cfv 6492  (class class class)co 7363  Basecbs 17177   ↾_s cress 17198  Grpcgrp 18907  SubGrpcsubg 19094  Ringcrg 20212  SubRingcsubrg 20548

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 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369

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 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-subg 19097  df-ring 20214  df-subrg 20549

This theorem is referenced by:  subrg0  20558  subrgbas  20560  subrgacl  20562  issubrg2  20571  subrgint  20574  resrhm  20580  resrhm2b  20581  rhmima  20583  subdrgint  20782  primefld0cl  20785  abvres  20810  zsssubrg  21407  gzrngunitlem  21414  zringlpirlem1  21444  zringcyg  21451  zringsubgval  21452  prmirred  21456  zndvds  21531  resubgval  21591  rzgrp  21605  issubassa2  21874  resspsrmul  21957  subrgpsr  21959  mplbas2  22025  gsumply1subr  22225  subrgnrg  24663  sranlm  24674  clmsub  25072  clmneg  25073  clmabs  25075  clmsubcl  25078  isncvsngp  25141  cphsqrtcl3  25179  tcphcph  25229  plypf1  26202  dvply2g  26276  taylply2  26358  circgrp  26541  circsubm  26542  jensenlem2  26976  amgmlem  26978  lgseisenlem4  27366  qrng0  27609  qrngneg  27611  subrgchr  33325  elrgspnlem4  33333  elrgspnsubrunlem2  33336  subrdom  33373  1fldgenq  33413  nn0archi  33437  idlinsubrg  33521  ressply1evls1  33655  ressply10g  33657  ressply1invg  33659  ressply1sub  33660  evls1subd  33662  vr1nz  33683  drgext0gsca  33783  fedgmullem1  33820  fedgmullem2  33821  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  irngss  33878  extdgfialglem1  33883  extdgfialglem2  33884  algextdeglem1  33908  algextdeglem2  33909  algextdeglem3  33910  algextdeglem4  33911  algextdeglem5  33912  rtelextdg2lem  33917  constrelextdg2  33938  2sqr3minply  33971  rezh  34160  qqhcn  34182  qqhucn  34183  fsumcnsrcl  43618  cnsrplycl  43619  rngunsnply  43621  amgmwlem  50299