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 |`s S )
	subg0.i	|- .0. = ( 0g ` G )
Assertion	subg0	|- ( S e. ( SubGrp ` G ) -> .0. = ( 0g ` H ) )

Proof

Step	Hyp	Ref	Expression
1		subg0.h	|- H = ( G |`s S )
2		subg0.i	|- .0. = ( 0g ` G )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4	1 3	ressplusg	|- ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
5	4	oveqd	|- ( S e. ( SubGrp ` G ) -> ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( ( 0g ` H ) ( +g ` H ) ( 0g ` H ) ) )
6	1	subggrp	|- ( S e. ( SubGrp ` G ) -> H e. Grp )
7		eqid	|- ( Base ` H ) = ( Base ` H )
8		eqid	|- ( 0g ` H ) = ( 0g ` H )
9	7 8	grpidcl	|- ( H e. Grp -> ( 0g ` H ) e. ( Base ` H ) )
10	6 9	syl	|- ( S e. ( SubGrp ` G ) -> ( 0g ` H ) e. ( Base ` H ) )
11		eqid	|- ( +g ` H ) = ( +g ` H )
12	7 11 8	grplid	|- ( ( H e. Grp /\ ( 0g ` H ) e. ( Base ` H ) ) -> ( ( 0g ` H ) ( +g ` H ) ( 0g ` H ) ) = ( 0g ` H ) )
13	6 10 12	syl2anc	|- ( S e. ( SubGrp ` G ) -> ( ( 0g ` H ) ( +g ` H ) ( 0g ` H ) ) = ( 0g ` H ) )
14	5 13	eqtrd	|- ( S e. ( SubGrp ` G ) -> ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( 0g ` H ) )
15		subgrcl	|- ( S e. ( SubGrp ` G ) -> G e. Grp )
16		eqid	|- ( Base ` G ) = ( Base ` G )
17	16	subgss	|- ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
18	1	subgbas	|- ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
19	10 18	eleqtrrd	|- ( S e. ( SubGrp ` G ) -> ( 0g ` H ) e. S )
20	17 19	sseldd	|- ( S e. ( SubGrp ` G ) -> ( 0g ` H ) e. ( Base ` G ) )
21	16 3 2	grpid	|- ( ( G e. Grp /\ ( 0g ` H ) e. ( Base ` G ) ) -> ( ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( 0g ` H ) <-> .0. = ( 0g ` H ) ) )
22	15 20 21	syl2anc	|- ( S e. ( SubGrp ` G ) -> ( ( ( 0g ` H ) ( +g ` G ) ( 0g ` H ) ) = ( 0g ` H ) <-> .0. = ( 0g ` H ) ) )
23	14 22	mpbid	|- ( S e. ( SubGrp ` G ) -> .0. = ( 0g ` H ) )