Theorem grpidd2

Description: Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd . (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	grpidd2.b	|- ( ph -> B = ( Base ` G ) )
	grpidd2.p	|- ( ph -> .+ = ( +g ` G ) )
	grpidd2.z	|- ( ph -> .0. e. B )
	grpidd2.i	|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
	grpidd2.j	|- ( ph -> G e. Grp )
Assertion	grpidd2	|- ( ph -> .0. = ( 0g ` G ) )

Proof

Step	Hyp	Ref	Expression
1		grpidd2.b	|- ( ph -> B = ( Base ` G ) )
2		grpidd2.p	|- ( ph -> .+ = ( +g ` G ) )
3		grpidd2.z	|- ( ph -> .0. e. B )
4		grpidd2.i	|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
5		grpidd2.j	|- ( ph -> G e. Grp )
6	2	oveqd	|- ( ph -> ( .0. .+ .0. ) = ( .0. ( +g ` G ) .0. ) )
7		oveq2	|- ( x = .0. -> ( .0. .+ x ) = ( .0. .+ .0. ) )
8		id	|- ( x = .0. -> x = .0. )
9	7 8	eqeq12d	|- ( x = .0. -> ( ( .0. .+ x ) = x <-> ( .0. .+ .0. ) = .0. ) )
10	4	ralrimiva	|- ( ph -> A. x e. B ( .0. .+ x ) = x )
11	9 10 3	rspcdva	|- ( ph -> ( .0. .+ .0. ) = .0. )
12	6 11	eqtr3d	|- ( ph -> ( .0. ( +g ` G ) .0. ) = .0. )
13	3 1	eleqtrd	|- ( ph -> .0. e. ( Base ` G ) )
14		eqid	|- ( Base ` G ) = ( Base ` G )
15		eqid	|- ( +g ` G ) = ( +g ` G )
16		eqid	|- ( 0g ` G ) = ( 0g ` G )
17	14 15 16	grpid	|- ( ( G e. Grp /\ .0. e. ( Base ` G ) ) -> ( ( .0. ( +g ` G ) .0. ) = .0. <-> ( 0g ` G ) = .0. ) )
18	5 13 17	syl2anc	|- ( ph -> ( ( .0. ( +g ` G ) .0. ) = .0. <-> ( 0g ` G ) = .0. ) )
19	12 18	mpbid	|- ( ph -> ( 0g ` G ) = .0. )
20	19	eqcomd	|- ( ph -> .0. = ( 0g ` G ) )