This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ∈ Grp ∧ A ∈ X ∧ O ⁡ A ∈ ℕ → K ⁡ A = O ⁡ A

Proof

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 ⊢ ⋅ G = ⋅ G
5 1 4 2 3 odf1o2 ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A ∈ ℕ → x ∈ 0 ..^ O ⁡ A ⟼ x ⋅ G A : 0 ..^ O ⁡ A ⟶ 1-1 onto K ⁡ A
6 ovex ⊢ 0 ..^ O ⁡ A ∈ V
7 6 f1oen ⊢ x ∈ 0 ..^ O ⁡ A ⟼ x ⋅ G A : 0 ..^ O ⁡ A ⟶ 1-1 onto K ⁡ A → 0 ..^ O ⁡ A ≈ K ⁡ A
8 hasheni ⊢ 0 ..^ O ⁡ A ≈ K ⁡ A → 0 ..^ O ⁡ A = K ⁡ A
9 5 7 8 3syl ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A ∈ ℕ → 0 ..^ O ⁡ A = K ⁡ A
10 1 2 odcl ⊢ A ∈ X → O ⁡ A ∈ ℕ 0
11 10 3ad2ant2 ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A ∈ ℕ → O ⁡ A ∈ ℕ 0
12 hashfzo0 ⊢ O ⁡ A ∈ ℕ 0 → 0 ..^ O ⁡ A = O ⁡ A
13 11 12 syl ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A ∈ ℕ → 0 ..^ O ⁡ A = O ⁡ A
14 9 13 eqtr3d ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A ∈ ℕ → K ⁡ A = O ⁡ A