Theorem od1

Description: The order of the group identity is 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 ‘ 𝐺 )
Assertion	od1	⊢ ( 𝐺 ∈ Grp → ( 𝑂 ‘ 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		od1.1	⊢ 𝑂 = ( od ‘ 𝐺 )
2		od1.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	3 2	grpidcl	⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
5		1nn	⊢ 1 ∈ ℕ
6	5	a1i	⊢ ( 𝐺 ∈ Grp → 1 ∈ ℕ )
7		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
8	3 7	mulg1	⊢ ( 0 ∈ ( Base ‘ 𝐺 ) → ( 1 ( .g ‘ 𝐺 ) 0 ) = 0 )
9	4 8	syl	⊢ ( 𝐺 ∈ Grp → ( 1 ( .g ‘ 𝐺 ) 0 ) = 0 )
10	3 1 7 2	odlem2	⊢ ( ( 0 ∈ ( Base ‘ 𝐺 ) ∧ 1 ∈ ℕ ∧ ( 1 ( .g ‘ 𝐺 ) 0 ) = 0 ) → ( 𝑂 ‘ 0 ) ∈ ( 1 ... 1 ) )
11	4 6 9 10	syl3anc	⊢ ( 𝐺 ∈ Grp → ( 𝑂 ‘ 0 ) ∈ ( 1 ... 1 ) )
12		elfz1eq	⊢ ( ( 𝑂 ‘ 0 ) ∈ ( 1 ... 1 ) → ( 𝑂 ‘ 0 ) = 1 )
13	11 12	syl	⊢ ( 𝐺 ∈ Grp → ( 𝑂 ‘ 0 ) = 1 )