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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odhash.o ⊢ 𝑂 = ( od ‘ 𝐺 )
odhash.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion odhash3 ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐾 ‘ { 𝐴 } ) ∈ Fin ) → ( 𝑂 ‘ 𝐴 ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 odhash.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odhash.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odhash.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
5 4 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐾 ‘ { 𝐴 } ) ∈ Fin ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
6 hashcl ⊢ ( ( 𝐾 ‘ { 𝐴 } ) ∈ Fin → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) ∈ ℕ0 )
7 6 nn0red ⊢ ( ( 𝐾 ‘ { 𝐴 } ) ∈ Fin → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) ∈ ℝ )
8 pnfnre ⊢ +∞ ∉ ℝ
9 8 neli ⊢ ¬ +∞ ∈ ℝ
10 1 2 3 odhash ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = +∞ )
11 10 eleq1d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
12 9 11 mtbiri ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) ∈ ℝ )
13 12 3expia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → ¬ ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) ∈ ℝ ) )
14 13 necon2ad ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) ∈ ℝ → ( 𝑂 ‘ 𝐴 ) ≠ 0 ) )
15 7 14 syl5 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐾 ‘ { 𝐴 } ) ∈ Fin → ( 𝑂 ‘ 𝐴 ) ≠ 0 ) )
16 15 3impia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐾 ‘ { 𝐴 } ) ∈ Fin ) → ( 𝑂 ‘ 𝐴 ) ≠ 0 )
17 elnnne0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ∧ ( 𝑂 ‘ 𝐴 ) ≠ 0 ) )
18 5 16 17 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐾 ‘ { 𝐴 } ) ∈ Fin ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
19 1 2 3 odhash2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = ( 𝑂 ‘ 𝐴 ) )
20 18 19 syld3an3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐾 ‘ { 𝐴 } ) ∈ Fin ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = ( 𝑂 ‘ 𝐴 ) )
21 20 eqcomd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐾 ‘ { 𝐴 } ) ∈ Fin ) → ( 𝑂 ‘ 𝐴 ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )