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 )