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 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = ( 𝑂 ‘ 𝐴 ) )