Theorem isgrpid2

Description: Properties showing that an element Z is the identity element of a group. (Contributed by NM, 7-Aug-2013)

	Ref	Expression
Hypotheses	grpinveu.b	|- B = ( Base ` G )
	grpinveu.p	|- .+ = ( +g ` G )
	grpinveu.o	|- .0. = ( 0g ` G )
Assertion	isgrpid2	|- ( G e. Grp -> ( ( Z e. B /\ ( Z .+ Z ) = Z ) <-> .0. = Z ) )

Proof

Step	Hyp	Ref	Expression
1		grpinveu.b	|- B = ( Base ` G )
2		grpinveu.p	|- .+ = ( +g ` G )
3		grpinveu.o	|- .0. = ( 0g ` G )
4	1 2 3	grpid	|- ( ( G e. Grp /\ Z e. B ) -> ( ( Z .+ Z ) = Z <-> .0. = Z ) )
5	4	biimpd	|- ( ( G e. Grp /\ Z e. B ) -> ( ( Z .+ Z ) = Z -> .0. = Z ) )
6	5	expimpd	|- ( G e. Grp -> ( ( Z e. B /\ ( Z .+ Z ) = Z ) -> .0. = Z ) )
7	1 3	grpidcl	|- ( G e. Grp -> .0. e. B )
8	1 2 3	grplid	|- ( ( G e. Grp /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
9	7 8	mpdan	|- ( G e. Grp -> ( .0. .+ .0. ) = .0. )
10	7 9	jca	|- ( G e. Grp -> ( .0. e. B /\ ( .0. .+ .0. ) = .0. ) )
11		eleq1	|- ( .0. = Z -> ( .0. e. B <-> Z e. B ) )
12		id	|- ( .0. = Z -> .0. = Z )
13	12 12	oveq12d	|- ( .0. = Z -> ( .0. .+ .0. ) = ( Z .+ Z ) )
14	13 12	eqeq12d	|- ( .0. = Z -> ( ( .0. .+ .0. ) = .0. <-> ( Z .+ Z ) = Z ) )
15	11 14	anbi12d	|- ( .0. = Z -> ( ( .0. e. B /\ ( .0. .+ .0. ) = .0. ) <-> ( Z e. B /\ ( Z .+ Z ) = Z ) ) )
16	10 15	syl5ibcom	|- ( G e. Grp -> ( .0. = Z -> ( Z e. B /\ ( Z .+ Z ) = Z ) ) )
17	6 16	impbid	|- ( G e. Grp -> ( ( Z e. B /\ ( Z .+ Z ) = Z ) <-> .0. = Z ) )