Theorem subrgsubg 20822

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 20821	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
2		ringgrp 20457	. . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp)
4		eqid 2761	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
5	4	subrgss 20817	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
6		eqid 2761	. . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴)
7	6	subrgring 20819	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring)
8		ringgrp 20457	. . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp)
9	7, 8	syl 18	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp)
10	4	issubg 19329	. 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 2145   ⊆ wss 3899  ‘cfv 6537  (class class class)co 7418  Basecbs 17380   ↾_s cress 17401  Grpcgrp 19137  SubGrpcsubg 19323  Ringcrg 20452  SubRingcsubrg 20814

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7421  df-subg 19326  df-ring 20454  df-subrg 20815

This theorem is used by:  subrg0  20824  subrgbas  20826  subrgacl  20828  issubrg2  20837  subrgint  20840  resrhm  20846  resrhm2b  20847  rhmima  20849  subdrgint  21053  primefld0cl  21056  abvres  21081  zsssubrg  21724  gzrngunitlem  21731  zringlpirlem1  21761  zringcyg  21768  zringsubgval  21769  prmirred  21773  zndvds  21848  resubgval  21908  rzgrp  21922  issubassa2  22193  resspsrmul  22276  subrgpsr  22278  mplbas2  22344  gsumply1subr  22544  subrgnrg  24985  sranlm  24996  clmsub  25394  clmneg  25395  clmabs  25397  clmsubcl  25400  isncvsngp  25463  cphsqrtcl3  25501  tcphcph  25551  plypf1  26524  dvply2g  26599  taylply2  26688  circgrp  26873  circsubm  26874  jensenlem2  27308  amgmlem  27310  lgseisenlem4  27698  qrng0  27941  qrngneg  27943  subrgchr  33790  elrgspnlem4  33799  elrgspnsubrunlem2  33802  subrdom  33839  1fldgenq  33877  nn0archi  33901  idlinsubrg  33974  ressply1evls1  34090  ressply10g  34092  ressply1invg  34094  ressply1sub  34095  evls1subd  34097  vr1nz  34118  drgext0gsca  34217  fedgmullem1  34254  fedgmullem2  34255  evls1fldgencl  34295  fldextrspunlsplem  34298  fldextrspunlsp  34299  irngss  34312  extdgfialglem1  34317  extdgfialglem2  34318  algextdeglem1  34342  algextdeglem2  34343  algextdeglem3  34344  algextdeglem4  34345  algextdeglem5  34346  rtelextdg2lem  34351  constrelextdg2  34372  2sqr3minply  34405  rezh  34594  qqhcn  34616  qqhucn  34617  fsumcnsrcl  44152  cnsrplycl  44153  rngunsnply  44155  amgmwlem  50956