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 ˙ = 0 G
odeq1.3 X = Base G
Assertion odeq1 G Grp A X O A = 1 A = 0 ˙

Proof

Step Hyp Ref Expression
1 od1.1 O = od G
2 od1.2 0 ˙ = 0 G
3 odeq1.3 X = Base G
4 oveq1 O A = 1 O A G A = 1 G A
5 4 eqcomd O A = 1 1 G A = O A G A
6 eqid G = G
7 3 6 mulg1 A X 1 G A = A
8 3 1 6 2 odid A X O A G A = 0 ˙
9 7 8 eqeq12d A X 1 G A = O A G A A = 0 ˙
10 9 adantl G Grp A X 1 G A = O A G A A = 0 ˙
11 5 10 syl5ib G Grp A X O A = 1 A = 0 ˙
12 1 2 od1 G Grp O 0 ˙ = 1
13 12 adantr G Grp A X O 0 ˙ = 1
14 fveqeq2 A = 0 ˙ O A = 1 O 0 ˙ = 1
15 13 14 syl5ibrcom G Grp A X A = 0 ˙ O A = 1
16 11 15 impbid G Grp A X O A = 1 A = 0 ˙