Theorem subg0

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)

	Ref	Expression
Hypotheses	subg0.h	$$⊢H=G{\upharpoonright }_{𝑠}S$$
	subg0.i	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	subg0	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}=0_H$$

Proof

Step	Hyp	Ref	Expression
1		subg0.h	$$⊢H=G{\upharpoonright }_{𝑠}S$$
2		subg0.i	$$⊢\underset{\dot{}}{0}=0_G$$
3		eqid	$$⊢{+}_G={+}_G$$
4	1 3	ressplusg	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to {+}_G={+}_H$$
5	4	oveqd	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to 0_H{+}_G{0}_H=0_H{+}_H{0}_H$$
6	1	subggrp	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to H\in \mathrm{Grp}$$
7		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
8		eqid	$$⊢0_H=0_H$$
9	7 8	grpidcl	$$⊢H\in \mathrm{Grp}\to 0_H\in {\mathrm{Base}}_H$$
10	6 9	syl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to 0_H\in {\mathrm{Base}}_H$$
11		eqid	$$⊢{+}_H={+}_H$$
12	7 11 8	grplid	$$⊢\left(H\in \mathrm{Grp}\wedge 0_H\in {\mathrm{Base}}_H\right)\to 0_H{+}_H{0}_H=0_H$$
13	6 10 12	syl2anc	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to 0_H{+}_H{0}_H=0_H$$
14	5 13	eqtrd	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to 0_H{+}_G{0}_H=0_H$$
15		subgrcl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
16		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
17	16	subgss	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\subseteq {\mathrm{Base}}_G$$
18	1	subgbas	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S={\mathrm{Base}}_H$$
19	10 18	eleqtrrd	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to 0_H\in S$$
20	17 19	sseldd	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to 0_H\in {\mathrm{Base}}_G$$
21	16 3 2	grpid	$$⊢\left(G\in \mathrm{Grp}\wedge 0_H\in {\mathrm{Base}}_G\right)\to \left(0_H{+}_G{0}_H=0_H\leftrightarrow \underset{\dot{}}{0}=0_H\right)$$
22	15 20 21	syl2anc	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to \left(0_H{+}_G{0}_H=0_H\leftrightarrow \underset{\dot{}}{0}=0_H\right)$$
23	14 22	mpbid	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}=0_H$$