Theorem subg0 19135

Description: A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)

Hypotheses

Ref	Expression
subg0.h	⊢ 𝐻 = (𝐺 ↾s 𝑆)
subg0.i	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
subg0	⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘𝐻))

Proof of Theorem subg0

Step	Hyp	Ref	Expression
1		subg0.h	. . . . 5 ⊢ 𝐻 = (𝐺 ↾s 𝑆)
2		eqid 2729	. . . . 5 ⊢ (+g‘𝐺) = (+g‘𝐺)
3	1, 2	ressplusg 17312	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (+g‘𝐺) = (+g‘𝐻))
4	3	oveqd 7442	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → ((0g‘𝐻)(+g‘𝐺)(0g‘𝐻)) = ((0g‘𝐻)(+g‘𝐻)(0g‘𝐻)))
5	1	subggrp 19132	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
6		eqid 2729	. . . . . 6 ⊢ (Base‘𝐻) = (Base‘𝐻)
7		eqid 2729	. . . . . 6 ⊢ (0g‘𝐻) = (0g‘𝐻)
8	6, 7	grpidcl 18968	. . . . 5 ⊢ (𝐻 ∈ Grp → (0g‘𝐻) ∈ (Base‘𝐻))
9	5, 8	syl 17	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (0g‘𝐻) ∈ (Base‘𝐻))
10		eqid 2729	. . . . 5 ⊢ (+g‘𝐻) = (+g‘𝐻)
11	6, 10, 7	grplid 18970	. . . 4 ⊢ ((𝐻 ∈ Grp ∧ (0g‘𝐻) ∈ (Base‘𝐻)) → ((0g‘𝐻)(+g‘𝐻)(0g‘𝐻)) = (0g‘𝐻))
12	5, 9, 11	syl2anc 582	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → ((0g‘𝐻)(+g‘𝐻)(0g‘𝐻)) = (0g‘𝐻))
13	4, 12	eqtrd 2769	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → ((0g‘𝐻)(+g‘𝐺)(0g‘𝐻)) = (0g‘𝐻))
14		subgrcl 19134	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
15		eqid 2729	. . . . 5 ⊢ (Base‘𝐺) = (Base‘𝐺)
16	15	subgss 19130	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺))
17	1	subgbas 19133	. . . . 5 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻))
18	9, 17	eleqtrrd 2832	. . . 4 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (0g‘𝐻) ∈ 𝑆)
19	16, 18	sseldd 3989	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (0g‘𝐻) ∈ (Base‘𝐺))
20		subg0.i	. . . 4 ⊢ 0 = (0g‘𝐺)
21	15, 2, 20	grpid 18978	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (0g‘𝐻) ∈ (Base‘𝐺)) → (((0g‘𝐻)(+g‘𝐺)(0g‘𝐻)) = (0g‘𝐻) ↔ 0 = (0g‘𝐻)))
22	14, 19, 21	syl2anc 582	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (((0g‘𝐻)(+g‘𝐺)(0g‘𝐻)) = (0g‘𝐻) ↔ 0 = (0g‘𝐻)))
23	13, 22	mpbid 231	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘𝐻))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2100  ‘cfv 6555  (class class class)co 7425  Basecbs 17221   ↾_s cress 17250  +_gcplusg 17274  0_gc0g 17462  Grpcgrp 18936  SubGrpcsubg 19123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5304  ax-nul 5311  ax-pow 5370  ax-pr 5434  ax-un 7746  ax-cnex 11218  ax-resscn 11219  ax-1cn 11220  ax-icn 11221  ax-addcl 11222  ax-addrcl 11223  ax-mulcl 11224  ax-mulrcl 11225  ax-mulcom 11226  ax-addass 11227  ax-mulass 11228  ax-distr 11229  ax-i2m1 11230  ax-1ne0 11231  ax-1rid 11232  ax-rnegex 11233  ax-rrecex 11234  ax-cnre 11235  ax-pre-lttri 11236  ax-pre-lttrn 11237  ax-pre-ltadd 11238  ax-pre-mulgt0 11239

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rmo 3372  df-reu 3373  df-rab 3428  df-v 3473  df-sbc 3786  df-csb 3902  df-dif 3959  df-un 3961  df-in 3963  df-ss 3973  df-pss 3976  df-nul 4333  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-iun 5005  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5581  df-eprel 5587  df-po 5595  df-so 5596  df-fr 5638  df-we 5640  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6314  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6507  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7381  df-ov 7428  df-oprab 7429  df-mpo 7430  df-om 7880  df-2nd 8007  df-frecs 8299  df-wrecs 8330  df-recs 8404  df-rdg 8443  df-er 8737  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11304  df-mnf 11305  df-xr 11306  df-ltxr 11307  df-le 11308  df-sub 11500  df-neg 11501  df-nn 12272  df-2 12334  df-sets 17174  df-slot 17192  df-ndx 17204  df-base 17222  df-ress 17251  df-plusg 17287  df-0g 17464  df-mgm 18641  df-sgrp 18720  df-mnd 18736  df-grp 18939  df-subg 19126

This theorem is referenced by:  subginv  19136  subg0cl  19137  subgmulg  19143  subgga  19303  gasubg  19305  sylow2blem2  19628  subgdmdprd  20043  pgpfaclem1  20090  subrng0  20546  subrg0  20572  subdrgint  20791  abvres  20819  rngqiprngimf1lem  21292  gzrngunitlem  21438  frlm0  21761  frlmgsum  21779  mpl0  22024  subgnm  24643  cphsubrglem  25206  qrng0  27660  suborng  33211  pwssplit4  42799