odhash3

Description: An element which generates a finite subgroup has order the size of that subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	odhash.x	$⊢ X = {Base}_{G}$
	odhash.o	$⊢ O = od (G)$
	odhash.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	odhash3	$⊢ (G \in Grp \land A \in X \land K (\{A\}) \in Fin) \to O (A) = \|K (\{A\})\|$

Step	Hyp	Ref	Expression
1		odhash.x	$⊢ X = {Base}_{G}$
2		odhash.o	$⊢ O = od (G)$
3		odhash.k	$⊢ K = mrCls (SubGrp (G))$
4	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
5	4	3ad2ant2	$⊢ (G \in Grp \land A \in X \land K (\{A\}) \in Fin) \to O (A) \in ℕ_{0}$
6		hashcl	$⊢ K (\{A\}) \in Fin \to \|K (\{A\})\| \in ℕ_{0}$
7	6	nn0red	$⊢ K (\{A\}) \in Fin \to \|K (\{A\})\| \in ℝ$
8		pnfnre	$⊢ +∞ \notin ℝ$
9	8	neli	$⊢ \neg +∞ \in ℝ$
10	1 2 3	odhash	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \|K (\{A\})\| = +∞$
11	10	eleq1d	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (\|K (\{A\})\| \in ℝ \leftrightarrow +∞ \in ℝ)$
12	9 11	mtbiri	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \neg \|K (\{A\})\| \in ℝ$
13	12	3expia	$⊢ (G \in Grp \land A \in X) \to (O (A) = 0 \to \neg \|K (\{A\})\| \in ℝ)$
14	13	necon2ad	$⊢ (G \in Grp \land A \in X) \to (\|K (\{A\})\| \in ℝ \to O (A) \neq 0)$
15	7 14	syl5	$⊢ (G \in Grp \land A \in X) \to (K (\{A\}) \in Fin \to O (A) \neq 0)$
16	15	3impia	$⊢ (G \in Grp \land A \in X \land K (\{A\}) \in Fin) \to O (A) \neq 0$
17		elnnne0	$⊢ O (A) \in ℕ \leftrightarrow (O (A) \in ℕ_{0} \land O (A) \neq 0)$
18	5 16 17	sylanbrc	$⊢ (G \in Grp \land A \in X \land K (\{A\}) \in Fin) \to O (A) \in ℕ$
19	1 2 3	odhash2	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|K (\{A\})\| = O (A)$
20	18 19	syld3an3	$⊢ (G \in Grp \land A \in X \land K (\{A\}) \in Fin) \to \|K (\{A\})\| = O (A)$
21	20	eqcomd	$⊢ (G \in Grp \land A \in X \land K (\{A\}) \in Fin) \to O (A) = \|K (\{A\})\|$

Metamath Proof Explorer