Theorem subg0cl 19344

Description: The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)

Hypothesis

Ref	Expression
subg0cl.i	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
subg0cl	⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)

Proof of Theorem subg0cl

Step	Hyp	Ref	Expression
1		eqid 2760	. . . 4 ⊢ (𝐺 ↾s 𝑆) = (𝐺 ↾s 𝑆)
2	1	subggrp 19339	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
3		eqid 2760	. . . 4 ⊢ (Base‘(𝐺 ↾s 𝑆)) = (Base‘(𝐺 ↾s 𝑆))
4		eqid 2760	. . . 4 ⊢ (0g‘(𝐺 ↾s 𝑆)) = (0g‘(𝐺 ↾s 𝑆))
5	3, 4	grpidcl 19176	. . 3 ⊢ ((𝐺 ↾s 𝑆) ∈ Grp → (0g‘(𝐺 ↾s 𝑆)) ∈ (Base‘(𝐺 ↾s 𝑆)))
6	2, 5	syl 18	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (0g‘(𝐺 ↾s 𝑆)) ∈ (Base‘(𝐺 ↾s 𝑆)))
7		subg0cl.i	. . 3 ⊢ 0 = (0g‘𝐺)
8	1, 7	subg0 19342	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘(𝐺 ↾s 𝑆)))
9	1	subgbas 19340	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺 ↾s 𝑆)))
10	6, 8, 9	3eltr4d 2875	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17387   ↾_s cress 17408  0_gc0g 17610  Grpcgrp 19144  SubGrpcsubg 19330

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-2 12405  df-sets 17342  df-slot 17360  df-ndx 17372  df-base 17388  df-ress 17409  df-plusg 17441  df-0g 17612  df-mgm 18816  df-sgrp 18908  df-mnd 18924  df-grp 19147  df-subg 19333

This theorem is used by:  subgmulgcl  19350  issubg3  19355  issubg4  19356  subgint  19361  trivsubgd  19363  eqger  19390  ghmpreima  19452  subgga  19514  gasubg  19516  sylow1lem5  19816  sylow2blem2  19835  sylow2blem3  19836  fislw  19839  sylow3lem3  19843  sylow3lem4  19844  lsm01  19885  lsm02  19886  lsmdisj  19895  lsmdisj2  19896  pj1lid  19915  pj1rid  19916  dmdprdd  20215  dprdfid  20233  dprdfeq0  20238  dprdsubg  20240  dprdres  20244  dprdz  20246  dprdsn  20252  dmdprdsplitlem  20253  dprddisj2  20255  dprd2da  20258  dmdprdsplit2lem  20261  ablfacrp  20282  ablfacrp2  20283  ablfac1c  20287  ablfac1eu  20289  pgpfac1lem3a  20292  pgpfac1lem3  20293  pgpfac1lem5  20295  pgpfaclem2  20298  pgpfaclem3  20299  prmgrpsimpgd  20330  primefld0cl  21063  abvres  21088  islss4  21237  dflidl2rng  21497  rnglidlrng  21535  rng2idl0  21561  rng2idlsubg0  21564  2idlcpblrng  21565  rng2idl1cntr  21601  subrgpsr  22285  mpllsslem  22307  0elcpmat  23040  opnsubg  24427  clssubg  24428  tgpconncompss  24433  plypf1  26531  dvply2g  26606  efsubm  26879  dchrptlem3  27593  gsumsubg  33649  elrgspnlem4  33848  subrdom  33888  nsgqus0  34003  nsgqusf1olem1  34006  ressply1evls1  34139  ressply10g  34141  ressply1invg  34143  vr1nz  34167  drgext0gsca  34266  fedgmullem2  34304  fldextrspunlsplem  34347  fldextrspunlsp  34348  extdgfialglem1  34366  extdgfialglem2  34367  algextdeglem4  34394  algextdeglem5  34395  rtelextdg2lem  34400  fsumcnsrcl  44211  cnsrplycl  44212  rngunsnply  44214