Theorem odeq1

Description: The group identity is the unique element of a group with order one. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypotheses	od1.1	|- O = ( od ` G )
	od1.2	|- .0. = ( 0g ` G )
	odeq1.3	|- X = ( Base ` G )
Assertion	odeq1	|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 1 <-> A = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		od1.1	|- O = ( od ` G )
2		od1.2	|- .0. = ( 0g ` G )
3		odeq1.3	|- X = ( Base ` G )
4		oveq1	|- ( ( O ` A ) = 1 -> ( ( O ` A ) ( .g ` G ) A ) = ( 1 ( .g ` G ) A ) )
5	4	eqcomd	|- ( ( O ` A ) = 1 -> ( 1 ( .g ` G ) A ) = ( ( O ` A ) ( .g ` G ) A ) )
6		eqid	|- ( .g ` G ) = ( .g ` G )
7	3 6	mulg1	|- ( A e. X -> ( 1 ( .g ` G ) A ) = A )
8	3 1 6 2	odid	|- ( A e. X -> ( ( O ` A ) ( .g ` G ) A ) = .0. )
9	7 8	eqeq12d	|- ( A e. X -> ( ( 1 ( .g ` G ) A ) = ( ( O ` A ) ( .g ` G ) A ) <-> A = .0. ) )
10	9	adantl	|- ( ( G e. Grp /\ A e. X ) -> ( ( 1 ( .g ` G ) A ) = ( ( O ` A ) ( .g ` G ) A ) <-> A = .0. ) )
11	5 10	syl5ib	|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 1 -> A = .0. ) )
12	1 2	od1	|- ( G e. Grp -> ( O ` .0. ) = 1 )
13	12	adantr	|- ( ( G e. Grp /\ A e. X ) -> ( O ` .0. ) = 1 )
14		fveqeq2	|- ( A = .0. -> ( ( O ` A ) = 1 <-> ( O ` .0. ) = 1 ) )
15	13 14	syl5ibrcom	|- ( ( G e. Grp /\ A e. X ) -> ( A = .0. -> ( O ` A ) = 1 ) )
16	11 15	impbid	|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 1 <-> A = .0. ) )