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 ⊢ 𝑂 = ( od ‘ 𝐺 )
od1.2 ⊢ 0 = ( 0g ‘ 𝐺 )
odeq1.3 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion odeq1 ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 1 ↔ 𝐴 = 0 ) )

Proof

Step Hyp Ref Expression
1 od1.1 ⊢ 𝑂 = ( od ‘ 𝐺 )
2 od1.2 ⊢ 0 = ( 0g ‘ 𝐺 )
3 odeq1.3 ⊢ 𝑋 = ( Base ‘ 𝐺 )
4 oveq1 ⊢ ( ( 𝑂 ‘ 𝐴 ) = 1 → ( ( 𝑂 ‘ 𝐴 ) ( .g ‘ 𝐺 ) 𝐴 ) = ( 1 ( .g ‘ 𝐺 ) 𝐴 ) )
5 4 eqcomd ⊢ ( ( 𝑂 ‘ 𝐴 ) = 1 → ( 1 ( .g ‘ 𝐺 ) 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) ( .g ‘ 𝐺 ) 𝐴 ) )
6 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
7 3 6 mulg1 ⊢ ( 𝐴 ∈ 𝑋 → ( 1 ( .g ‘ 𝐺 ) 𝐴 ) = 𝐴 )
8 3 1 6 2 odid ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) ( .g ‘ 𝐺 ) 𝐴 ) = 0 )
9 7 8 eqeq12d ⊢ ( 𝐴 ∈ 𝑋 → ( ( 1 ( .g ‘ 𝐺 ) 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) ( .g ‘ 𝐺 ) 𝐴 ) ↔ 𝐴 = 0 ) )
10 9 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 ( .g ‘ 𝐺 ) 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) ( .g ‘ 𝐺 ) 𝐴 ) ↔ 𝐴 = 0 ) )
11 5 10 imbitrid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 1 → 𝐴 = 0 ) )
12 1 2 od1 ⊢ ( 𝐺 ∈ Grp → ( 𝑂 ‘ 0 ) = 1 )
13 12 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 0 ) = 1 )
14 fveqeq2 ⊢ ( 𝐴 = 0 → ( ( 𝑂 ‘ 𝐴 ) = 1 ↔ ( 𝑂 ‘ 0 ) = 1 ) )
15 13 14 syl5ibrcom ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 0 → ( 𝑂 ‘ 𝐴 ) = 1 ) )
16 11 15 impbid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 1 ↔ 𝐴 = 0 ) )