od1

Description: The order of the group identity is one. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 23-Sep-2015)

Step	Hyp	Ref	Expression
1		od1.1	$⊢ O = od (G)$
2		od1.2	$⊢ \underset{˙}{0} = 0_{G}$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4	3 2	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in {Base}_{G}$
5		1nn	$⊢ 1 \in ℕ$
6	5	a1i	$⊢ G \in Grp \to 1 \in ℕ$
7		eqid	$⊢ \cdot_{G} = \cdot_{G}$
8	3 7	mulg1	$⊢ \underset{˙}{0} \in {Base}_{G} \to 1 \cdot_{G} \underset{˙}{0} = \underset{˙}{0}$
9	4 8	syl	$⊢ G \in Grp \to 1 \cdot_{G} \underset{˙}{0} = \underset{˙}{0}$
10	3 1 7 2	odlem2	$⊢ (\underset{˙}{0} \in {Base}_{G} \land 1 \in ℕ \land 1 \cdot_{G} \underset{˙}{0} = \underset{˙}{0}) \to O (\underset{˙}{0}) \in (1 \dots 1)$
11	4 6 9 10	syl3anc	$⊢ G \in Grp \to O (\underset{˙}{0}) \in (1 \dots 1)$
12		elfz1eq	$⊢ O (\underset{˙}{0}) \in (1 \dots 1) \to O (\underset{˙}{0}) = 1$
13	11 12	syl	$⊢ G \in Grp \to O (\underset{˙}{0}) = 1$

Metamath Proof Explorer