Theorem subg0cl 19373

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 2763	. . . 4 ⊢ (𝐺 ↾s 𝑆) = (𝐺 ↾s 𝑆)
2	1	subggrp 19368	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
3		eqid 2763	. . . 4 ⊢ (Base‘(𝐺 ↾s 𝑆)) = (Base‘(𝐺 ↾s 𝑆))
4		eqid 2763	. . . 4 ⊢ (0g‘(𝐺 ↾s 𝑆)) = (0g‘(𝐺 ↾s 𝑆))
5	3, 4	grpidcl 19205	. . 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 19371	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘(𝐺 ↾s 𝑆)))
9	1	subgbas 19369	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺 ↾s 𝑆)))
10	6, 8, 9	3eltr4d 2879	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416   ↾_s cress 17437  0_gc0g 17639  Grpcgrp 19173  SubGrpcsubg 19359

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 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  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-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  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 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-nn 12363  df-2 12432  df-sets 17371  df-slot 17389  df-ndx 17401  df-base 17417  df-ress 17438  df-plusg 17470  df-0g 17641  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176  df-subg 19362

This theorem is used by:  subgmulgcl  19379  issubg3  19384  issubg4  19385  subgint  19390  trivsubgd  19392  eqger  19419  ghmpreima  19481  subgga  19544  gasubg  19546  sylow1lem5  19846  sylow2blem2  19865  sylow2blem3  19866  fislw  19869  sylow3lem3  19873  sylow3lem4  19874  lsm01  19915  lsm02  19916  lsmdisj  19925  lsmdisj2  19926  pj1lid  19945  pj1rid  19946  dmdprdd  20245  dprdfid  20263  dprdfeq0  20268  dprdsubg  20270  dprdres  20274  dprdz  20276  dprdsn  20282  dmdprdsplitlem  20283  dprddisj2  20285  dprd2da  20288  dmdprdsplit2lem  20291  ablfacrp  20312  ablfacrp2  20313  ablfac1c  20317  ablfac1eu  20319  pgpfac1lem3a  20322  pgpfac1lem3  20323  pgpfac1lem5  20325  pgpfaclem2  20328  pgpfaclem3  20329  prmgrpsimpgd  20360  primefld0cl  21093  abvres  21118  islss4  21267  dflidl2rng  21527  rnglidlrng  21565  rng2idl0  21591  rng2idlsubg0  21594  2idlcpblrng  21595  rng2idl1cntr  21631  subrgpsr  22315  mpllsslem  22337  0elcpmat  23070  opnsubg  24457  clssubg  24458  tgpconncompss  24463  plypf1  26561  dvply2g  26636  efsubm  26909  dchrptlem3  27623  gsumsubg  33677  elrgspnlem4  33876  subrdom  33916  nsgqus0  34031  nsgqusf1olem1  34034  ressply1evls1  34167  ressply10g  34169  ressply1invg  34171  vr1nz  34195  drgext0gsca  34294  fedgmullem2  34332  fldextrspunlsplem  34375  fldextrspunlsp  34376  extdgfialglem1  34394  extdgfialglem2  34395  algextdeglem4  34422  algextdeglem5  34423  rtelextdg2lem  34428  fsumcnsrcl  44360  cnsrplycl  44361  rngunsnply  44363