Theorem subrgsubg 20880

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 20879	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20515	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2763	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20875	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2763	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20877	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20515	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19386	. 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 2147   ⊆ wss 3900  ‘cfv 6566  (class class class)co 7451  Basecbs 17431   ↾_s cress 17452  Grpcgrp 19194  SubGrpcsubg 19380  Ringcrg 20510  SubRingcsubrg 20872

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fv 6574  df-ov 7454  df-subg 19383  df-ring 20512  df-subrg 20873

This theorem is used by:  subrg0  20882  subrgbas  20884  subrgacl  20886  issubrg2  20895  subrgint  20898  resrhm  20904  resrhm2b  20905  rhmima  20907  subdrgint  21111  primefld0cl  21114  abvres  21139  fsumcnsrcl  21777  zsssubrg  21785  gzrngunitlem  21792  zringlpirlem1  21823  zringcyg  21830  zringsubgval  21831  prmirred  21835  zndvds  21910  resubgval  21970  rzgrp  21984  issubassa2  22255  resspsrmul  22338  subrgpsr  22340  mplbas2  22406  gsumply1subr  22606  subrgnrg  25047  sranlm  25058  clmsub  25456  clmneg  25457  clmabs  25459  clmsubcl  25462  isncvsngp  25525  cphsqrtcl3  25563  tcphcph  25613  plypf1  26586  dvply2g  26661  cnsrplycl  26692  rngunsnply  26693  taylply2  26752  circgrp  26937  circsubm  26938  jensenlem2  27372  amgmlem  27374  lgseisenlem4  27762  qrng0  28005  qrngneg  28007  subrgchr  33896  elrgspnlem4  33905  elrgspnsubrunlem2  33908  subrdom  33945  1fldgenq  33988  nn0archi  34012  idlinsubrg  34085  ressply1evls1  34200  ressply10g  34202  ressply1invg  34204  ressply1sub  34205  evls1subd  34207  vr1nz  34228  evls1rgspncl  34248  rngunsnply1chr2lem2  34251  drgext0gsca  34335  fedgmullem1  34372  fedgmullem2  34373  evls1fldgencl  34413  fldextrspunlsplem  34416  fldextrspunlsp  34417  irngss  34430  extdgfialglem1  34435  extdgfialglem2  34436  algextdeglem1  34460  algextdeglem2  34461  algextdeglem3  34462  algextdeglem4  34463  algextdeglem5  34464  rtelextdg2lem  34469  constrelextdg2  34490  2sqr3minply  34523  rezh  34712  qqhcn  34734  qqhucn  34735  amgmwlem  51415