odhash2

Description: If an element has nonzero order, it generates a subgroup with size equal to the order. (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	odhash2	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|K (\{A\})\| = O (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		eqid	$⊢ \cdot_{G} = \cdot_{G}$
5	1 4 2 3	odf1o2	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (x \in (0 ..^O (A)) ⟼ x \cdot_{G} A) : (0 ..^O (A)) \underset{1-1 onto}{⟶} K (\{A\})$
6		ovex	$⊢ (0 ..^O (A)) \in V$
7	6	f1oen	$⊢ (x \in (0 ..^O (A)) ⟼ x \cdot_{G} A) : (0 ..^O (A)) \underset{1-1 onto}{⟶} K (\{A\}) \to (0 ..^O (A)) \approx K (\{A\})$
8		hasheni	$⊢ (0 ..^O (A)) \approx K (\{A\}) \to \|(0 ..^O (A))\| = \|K (\{A\})\|$
9	5 7 8	3syl	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|(0 ..^O (A))\| = \|K (\{A\})\|$
10	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
11	10	3ad2ant2	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to O (A) \in ℕ_{0}$
12		hashfzo0	$⊢ O (A) \in ℕ_{0} \to \|(0 ..^O (A))\| = O (A)$
13	11 12	syl	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|(0 ..^O (A))\| = O (A)$
14	9 13	eqtr3d	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|K (\{A\})\| = O (A)$

Metamath Proof Explorer