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 
|- O = ( od ` G )
od1.2 
|- .0. = ( 0g ` G )
Assertion od1 
|- ( G e. Grp -> ( O ` .0. ) = 1 )

Proof

Step Hyp Ref Expression
1 od1.1 
 |-  O = ( od ` G )
2 od1.2 
 |-  .0. = ( 0g ` G )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 3 2 grpidcl 
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
5 1nn 
 |-  1 e. NN
6 5 a1i 
 |-  ( G e. Grp -> 1 e. NN )
7 eqid 
 |-  ( .g ` G ) = ( .g ` G )
8 3 7 mulg1 
 |-  ( .0. e. ( Base ` G ) -> ( 1 ( .g ` G ) .0. ) = .0. )
9 4 8 syl 
 |-  ( G e. Grp -> ( 1 ( .g ` G ) .0. ) = .0. )
10 3 1 7 2 odlem2 
 |-  ( ( .0. e. ( Base ` G ) /\ 1 e. NN /\ ( 1 ( .g ` G ) .0. ) = .0. ) -> ( O ` .0. ) e. ( 1 ... 1 ) )
11 4 6 9 10 syl3anc 
 |-  ( G e. Grp -> ( O ` .0. ) e. ( 1 ... 1 ) )
12 elfz1eq 
 |-  ( ( O ` .0. ) e. ( 1 ... 1 ) -> ( O ` .0. ) = 1 )
13 11 12 syl 
 |-  ( G e. Grp -> ( O ` .0. ) = 1 )