Theorem subg0cl 19174

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 2740	. . . 4 ⊢ (𝐺 ↾s 𝑆) = (𝐺 ↾s 𝑆)
2	1	subggrp 19169	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
3		eqid 2740	. . . 4 ⊢ (Base‘(𝐺 ↾s 𝑆)) = (Base‘(𝐺 ↾s 𝑆))
4		eqid 2740	. . . 4 ⊢ (0g‘(𝐺 ↾s 𝑆)) = (0g‘(𝐺 ↾s 𝑆))
5	3, 4	grpidcl 19005	. . 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 19172	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘(𝐺 ↾s 𝑆)))
9	1	subgbas 19170	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺 ↾s 𝑆)))
10	6, 8, 9	3eltr4d 2859	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  Basecbs 17258   ↾_s cress 17287  0_gc0g 17499  Grpcgrp 18973  SubGrpcsubg 19160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-subg 19163

This theorem is referenced by:  subgmulgcl  19179  issubg3  19184  issubg4  19185  subgint  19190  trivsubgd  19193  eqger  19218  ghmpreima  19278  subgga  19340  gasubg  19342  sylow1lem5  19644  sylow2blem2  19663  sylow2blem3  19664  fislw  19667  sylow3lem3  19671  sylow3lem4  19672  lsm01  19713  lsm02  19714  lsmdisj  19723  lsmdisj2  19724  pj1lid  19743  pj1rid  19744  dmdprdd  20043  dprdfid  20061  dprdfeq0  20066  dprdsubg  20068  dprdres  20072  dprdz  20074  dprdsn  20080  dmdprdsplitlem  20081  dprddisj2  20083  dprd2da  20086  dmdprdsplit2lem  20089  ablfacrp  20110  ablfacrp2  20111  ablfac1c  20115  ablfac1eu  20117  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem5  20123  pgpfaclem2  20126  pgpfaclem3  20127  prmgrpsimpgd  20158  primefld0cl  20829  abvres  20854  islss4  20983  dflidl2rng  21251  rnglidlrng  21280  rng2idl0  21300  rng2idlsubg0  21303  2idlcpblrng  21304  rng2idl1cntr  21338  subrgpsr  22021  mpllsslem  22043  0elcpmat  22749  opnsubg  24137  clssubg  24138  tgpconncompss  24143  plypf1  26271  dvply2g  26344  dvply2gOLD  26345  efsubm  26611  dchrptlem3  27328  gsumsubg  33029  subrdom  33254  nsgqus0  33403  nsgqusf1olem1  33406  ressply10g  33557  ressply1invg  33559  drgext0gsca  33606  fedgmullem2  33643  algextdeglem4  33711  algextdeglem5  33712  rtelextdg2lem  33717  fsumcnsrcl  43123  cnsrplycl  43124  rngunsnply  43130