Theorem subrgsubg 20545

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 20544	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20210	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2737	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20540	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2737	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20542	. . 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 1345	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  ‘cfv 6492  (class class class)co 7360  Basecbs 17170   ↾_s cress 17191  Grpcgrp 18900  SubGrpcsubg 19087  Ringcrg 20205  SubRingcsubrg 20537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 7363  df-subg 19090  df-ring 20207  df-subrg 20538

This theorem is referenced by:  subrg0  20547  subrgbas  20549  subrgacl  20551  issubrg2  20560  subrgint  20563  resrhm  20569  resrhm2b  20570  rhmima  20572  subdrgint  20771  primefld0cl  20774  abvres  20799  zsssubrg  21415  gzrngunitlem  21422  zringlpirlem1  21452  zringcyg  21459  zringsubgval  21460  prmirred  21464  zndvds  21539  resubgval  21599  rzgrp  21613  issubassa2  21882  resspsrmul  21964  subrgpsr  21966  mplbas2  22030  gsumply1subr  22207  subrgnrg  24648  sranlm  24659  clmsub  25057  clmneg  25058  clmabs  25060  clmsubcl  25063  isncvsngp  25126  cphsqrtcl3  25164  tcphcph  25214  plypf1  26187  dvply2g  26261  dvply2gOLD  26262  taylply2  26344  taylply2OLD  26345  circgrp  26529  circsubm  26530  jensenlem2  26965  amgmlem  26967  lgseisenlem4  27355  qrng0  27598  qrngneg  27600  subrgchr  33313  elrgspnlem4  33321  elrgspnsubrunlem2  33324  subrdom  33361  1fldgenq  33398  nn0archi  33422  idlinsubrg  33506  ressply1evls1  33640  ressply10g  33642  ressply1invg  33644  ressply1sub  33645  evls1subd  33647  vr1nz  33668  drgext0gsca  33751  fedgmullem1  33789  fedgmullem2  33790  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  irngss  33847  extdgfialglem1  33852  extdgfialglem2  33853  algextdeglem1  33877  algextdeglem2  33878  algextdeglem3  33879  algextdeglem4  33880  algextdeglem5  33881  rtelextdg2lem  33886  constrelextdg2  33907  2sqr3minply  33940  rezh  34129  qqhcn  34151  qqhucn  34152  fsumcnsrcl  43612  cnsrplycl  43613  rngunsnply  43615  amgmwlem  50289