Theorem grpid

Description: Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		grpinveu.b	|- B = ( Base ` G )
2		grpinveu.p	|- .+ = ( +g ` G )
3		grpinveu.o	|- .0. = ( 0g ` G )
4		eqcom	|- ( .0. = X <-> X = .0. )
5	1 3	grpidcl	|- ( G e. Grp -> .0. e. B )
6	1 2	grprcan	|- ( ( G e. Grp /\ ( X e. B /\ .0. e. B /\ X e. B ) ) -> ( ( X .+ X ) = ( .0. .+ X ) <-> X = .0. ) )
7	6	3exp2	|- ( G e. Grp -> ( X e. B -> ( .0. e. B -> ( X e. B -> ( ( X .+ X ) = ( .0. .+ X ) <-> X = .0. ) ) ) ) )
8	5 7	mpid	|- ( G e. Grp -> ( X e. B -> ( X e. B -> ( ( X .+ X ) = ( .0. .+ X ) <-> X = .0. ) ) ) )
9	8	pm2.43d	|- ( G e. Grp -> ( X e. B -> ( ( X .+ X ) = ( .0. .+ X ) <-> X = .0. ) ) )
10	9	imp	|- ( ( G e. Grp /\ X e. B ) -> ( ( X .+ X ) = ( .0. .+ X ) <-> X = .0. ) )
11	1 2 3	grplid	|- ( ( G e. Grp /\ X e. B ) -> ( .0. .+ X ) = X )
12	11	eqeq2d	|- ( ( G e. Grp /\ X e. B ) -> ( ( X .+ X ) = ( .0. .+ X ) <-> ( X .+ X ) = X ) )
13	10 12	bitr3d	|- ( ( G e. Grp /\ X e. B ) -> ( X = .0. <-> ( X .+ X ) = X ) )
14	4 13	bitr2id	|- ( ( G e. Grp /\ X e. B ) -> ( ( X .+ X ) = X <-> .0. = X ) )