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

Proof

Step Hyp Ref Expression
1 odhash.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odhash.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odhash.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
5 1 4 2 3 odf1o2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) )
6 ovex ⊢ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∈ V
7 6 f1oen ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) → ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ≈ ( 𝐾 ‘ { 𝐴 } ) )
8 hasheni ⊢ ( ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ≈ ( 𝐾 ‘ { 𝐴 } ) → ( ♯ ‘ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )
9 5 7 8 3syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )
10 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
11 10 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
12 hashfzo0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ 𝐴 ) )
13 11 12 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ 𝐴 ) )
14 9 13 eqtr3d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = ( 𝑂 ‘ 𝐴 ) )