This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrid 
 |-  ( ( 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. ) )