Theorem subg0cl 19104

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 2734	. . . 4 ⊢ (𝐺 ↾s 𝑆) = (𝐺 ↾s 𝑆)
2	1	subggrp 19099	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
3		eqid 2734	. . . 4 ⊢ (Base‘(𝐺 ↾s 𝑆)) = (Base‘(𝐺 ↾s 𝑆))
4		eqid 2734	. . . 4 ⊢ (0g‘(𝐺 ↾s 𝑆)) = (0g‘(𝐺 ↾s 𝑆))
5	3, 4	grpidcl 18935	. . 3 ⊢ ((𝐺 ↾s 𝑆) ∈ Grp → (0g‘(𝐺 ↾s 𝑆)) ∈ (Base‘(𝐺 ↾s 𝑆)))
6	2, 5	syl 17	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (0g‘(𝐺 ↾s 𝑆)) ∈ (Base‘(𝐺 ↾s 𝑆)))
7		subg0cl.i	. . 3 ⊢ 0 = (0g‘𝐺)
8	1, 7	subg0 19102	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘(𝐺 ↾s 𝑆)))
9	1	subgbas 19100	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺 ↾s 𝑆)))
10	6, 8, 9	3eltr4d 2848	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ‘cfv 6528  (class class class)co 7400  Basecbs 17215   ↾_s cress 17238  0_gc0g 17440  Grpcgrp 18903  SubGrpcsubg 19090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-cnex 11178  ax-resscn 11179  ax-1cn 11180  ax-icn 11181  ax-addcl 11182  ax-addrcl 11183  ax-mulcl 11184  ax-mulrcl 11185  ax-mulcom 11186  ax-addass 11187  ax-mulass 11188  ax-distr 11189  ax-i2m1 11190  ax-1ne0 11191  ax-1rid 11192  ax-rnegex 11193  ax-rrecex 11194  ax-cnre 11195  ax-pre-lttri 11196  ax-pre-lttrn 11197  ax-pre-ltadd 11198  ax-pre-mulgt0 11199

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-iun 4967  df-br 5118  df-opab 5180  df-mpt 5200  df-tr 5228  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6288  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7857  df-2nd 7984  df-frecs 8275  df-wrecs 8306  df-recs 8380  df-rdg 8419  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268  df-sub 11461  df-neg 11462  df-nn 12234  df-2 12296  df-sets 17170  df-slot 17188  df-ndx 17200  df-base 17216  df-ress 17239  df-plusg 17271  df-0g 17442  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-grp 18906  df-subg 19093

This theorem is referenced by:  subgmulgcl  19109  issubg3  19114  issubg4  19115  subgint  19120  trivsubgd  19123  eqger  19148  ghmpreima  19208  subgga  19270  gasubg  19272  sylow1lem5  19570  sylow2blem2  19589  sylow2blem3  19590  fislw  19593  sylow3lem3  19597  sylow3lem4  19598  lsm01  19639  lsm02  19640  lsmdisj  19649  lsmdisj2  19650  pj1lid  19669  pj1rid  19670  dmdprdd  19969  dprdfid  19987  dprdfeq0  19992  dprdsubg  19994  dprdres  19998  dprdz  20000  dprdsn  20006  dmdprdsplitlem  20007  dprddisj2  20009  dprd2da  20012  dmdprdsplit2lem  20015  ablfacrp  20036  ablfacrp2  20037  ablfac1c  20041  ablfac1eu  20043  pgpfac1lem3a  20046  pgpfac1lem3  20047  pgpfac1lem5  20049  pgpfaclem2  20052  pgpfaclem3  20053  prmgrpsimpgd  20084  primefld0cl  20753  abvres  20778  islss4  20906  dflidl2rng  21166  rnglidlrng  21195  rng2idl0  21215  rng2idlsubg0  21218  2idlcpblrng  21219  rng2idl1cntr  21253  subrgpsr  21925  mpllsslem  21947  0elcpmat  22647  opnsubg  24033  clssubg  24034  tgpconncompss  24039  plypf1  26156  dvply2g  26231  dvply2gOLD  26232  efsubm  26498  dchrptlem3  27215  gsumsubg  32977  elrgspnlem4  33177  subrdom  33216  nsgqus0  33362  nsgqusf1olem1  33365  ressply10g  33516  ressply1invg  33518  drgext0gsca  33566  fedgmullem2  33605  fldextrspunlsplem  33649  fldextrspunlsp  33650  algextdeglem4  33689  algextdeglem5  33690  rtelextdg2lem  33695  fsumcnsrcl  43122  cnsrplycl  43123  rngunsnply  43125