Theorem subrgsubg 20705

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 20704	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20343	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2765	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20700	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2765	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20702	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20343	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19215	. 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 2146   ⊆ wss 3906  ‘cfv 6540  (class class class)co 7416  Basecbs 17286   ↾_s cress 17307  Grpcgrp 19023  SubGrpcsubg 19209  Ringcrg 20338  SubRingcsubrg 20697

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7419  df-subg 19212  df-ring 20340  df-subrg 20698

This theorem is used by:  subrg0  20707  subrgbas  20709  subrgacl  20711  issubrg2  20720  subrgint  20723  resrhm  20729  resrhm2b  20730  rhmima  20732  subdrgint  20935  primefld0cl  20938  abvres  20963  zsssubrg  21604  gzrngunitlem  21611  zringlpirlem1  21641  zringcyg  21648  zringsubgval  21649  prmirred  21653  zndvds  21728  resubgval  21788  rzgrp  21802  issubassa2  22071  resspsrmul  22154  subrgpsr  22156  mplbas2  22222  gsumply1subr  22422  subrgnrg  24859  sranlm  24870  clmsub  25268  clmneg  25269  clmabs  25271  clmsubcl  25274  isncvsngp  25337  cphsqrtcl3  25375  tcphcph  25425  plypf1  26398  dvply2g  26475  taylply2  26560  circgrp  26746  circsubm  26747  jensenlem2  27181  amgmlem  27183  lgseisenlem4  27571  qrng0  27814  qrngneg  27816  subrgchr  33579  elrgspnlem4  33588  elrgspnsubrunlem2  33591  subrdom  33628  1fldgenq  33666  nn0archi  33690  idlinsubrg  33762  ressply1evls1  33878  ressply10g  33880  ressply1invg  33882  ressply1sub  33883  evls1subd  33885  vr1nz  33906  drgext0gsca  34005  fedgmullem1  34042  fedgmullem2  34043  evls1fldgencl  34083  fldextrspunlsplem  34086  fldextrspunlsp  34087  irngss  34100  extdgfialglem1  34105  extdgfialglem2  34106  algextdeglem1  34130  algextdeglem2  34131  algextdeglem3  34132  algextdeglem4  34133  algextdeglem5  34134  rtelextdg2lem  34139  constrelextdg2  34160  2sqr3minply  34193  rezh  34382  qqhcn  34404  qqhucn  34405  fsumcnsrcl  43926  cnsrplycl  43927  rngunsnply  43929  amgmwlem  50683