Metamath Proof Explorer

Theorem 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 ∈ Grp ∧ A ∈ X ∧ K ⁡ A ∈ Fin → O ⁡ A = K ⁡ 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 1 2 odcl ⊢ A ∈ X → O ⁡ A ∈ ℕ 0
5 4 3ad2ant2 ⊢ G ∈ Grp ∧ A ∈ X ∧ K ⁡ A ∈ Fin → O ⁡ A ∈ ℕ 0
6 hashcl ⊢ K ⁡ A ∈ Fin → K ⁡ A ∈ ℕ 0
7 6 nn0red ⊢ K ⁡ A ∈ Fin → K ⁡ A ∈ ℝ
8 pnfnre ⊢ +∞ ∉ ℝ
9 8 neli ⊢ ¬ +∞ ∈ ℝ
10 1 2 3 odhash ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → K ⁡ A = +∞
11 10 eleq1d ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → K ⁡ A ∈ ℝ ↔ +∞ ∈ ℝ
12 9 11 mtbiri ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → ¬ K ⁡ A ∈ ℝ
13 12 3expia ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A = 0 → ¬ K ⁡ A ∈ ℝ
14 13 necon2ad ⊢ G ∈ Grp ∧ A ∈ X → K ⁡ A ∈ ℝ → O ⁡ A ≠ 0
15 7 14 syl5 ⊢ G ∈ Grp ∧ A ∈ X → K ⁡ A ∈ Fin → O ⁡ A ≠ 0
16 15 3impia ⊢ G ∈ Grp ∧ A ∈ X ∧ K ⁡ A ∈ Fin → O ⁡ A ≠ 0
17 elnnne0 ⊢ O ⁡ A ∈ ℕ ↔ O ⁡ A ∈ ℕ 0 ∧ O ⁡ A ≠ 0
18 5 16 17 sylanbrc ⊢ G ∈ Grp ∧ A ∈ X ∧ K ⁡ A ∈ Fin → O ⁡ A ∈ ℕ
19 1 2 3 odhash2 ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A ∈ ℕ → K ⁡ A = O ⁡ A
20 18 19 syld3an3 ⊢ G ∈ Grp ∧ A ∈ X ∧ K ⁡ A ∈ Fin → K ⁡ A = O ⁡ A
21 20 eqcomd ⊢ G ∈ Grp ∧ A ∈ X ∧ K ⁡ A ∈ Fin → O ⁡ A = K ⁡ A