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 ˙ = 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 imbitrid ⊢ 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 ˙