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=\mathrm{od}\left(G\right)$$
	od1.2	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	od1	$$⊢G\in \mathrm{Grp}\to O\left(\underset{\dot{}}{0}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		od1.1	$$⊢O=\mathrm{od}\left(G\right)$$
2		od1.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4	3 2	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
5		1nn	$$⊢1\in \mathbb{N}$$
6	5	a1i	$$⊢G\in \mathrm{Grp}\to 1\in \mathbb{N}$$
7		eqid	$$⊢{\cdot }_G={\cdot }_G$$
8	3 7	mulg1	$$⊢\underset{\dot{}}{0}\in {\mathrm{Base}}_G\to 1{\cdot }_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
9	4 8	syl	$$⊢G\in \mathrm{Grp}\to 1{\cdot }_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
10	3 1 7 2	odlem2	$$⊢\left(\underset{\dot{}}{0}\in {\mathrm{Base}}_G\wedge 1\in \mathbb{N}\wedge 1{\cdot }_G\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\to O\left(\underset{\dot{}}{0}\right)\in \left(1\dots 1\right)$$
11	4 6 9 10	syl3anc	$$⊢G\in \mathrm{Grp}\to O\left(\underset{\dot{}}{0}\right)\in \left(1\dots 1\right)$$
12		elfz1eq	$$⊢O\left(\underset{\dot{}}{0}\right)\in \left(1\dots 1\right)\to O\left(\underset{\dot{}}{0}\right)=1$$
13	11 12	syl	$$⊢G\in \mathrm{Grp}\to O\left(\underset{\dot{}}{0}\right)=1$$