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 ) )