This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )