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

Metamath Proof Explorer

Theorem odcl2

Description: The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses odcl2.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl2.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion odcl2 ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 odcl2.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl2.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
4 3 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
5 elnn0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
6 4 5 sylib ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
7 6 ord ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ¬ ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) = 0 ) )
8 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
9 eqid ⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) )
10 1 2 8 9 odinf ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin )
11 1 2 8 9 odf1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 ↔ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1→ 𝑋 ) )
12 11 biimp3a ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1→ 𝑋 )
13 f1f ⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1→ 𝑋 → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ ⟶ 𝑋 )
14 frn ⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ ⟶ 𝑋 → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 )
15 ssfi ⊢ ( ( 𝑋 ∈ Fin ∧ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin )
16 15 expcom ⊢ ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 → ( 𝑋 ∈ Fin → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin ) )
17 12 13 14 16 4syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑋 ∈ Fin → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin ) )
18 10 17 mtod ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ 𝑋 ∈ Fin )
19 18 3expia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → ¬ 𝑋 ∈ Fin ) )
20 7 19 syld ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ¬ ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ¬ 𝑋 ∈ Fin ) )
21 20 con4d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 ∈ Fin → ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) )
22 21 3impia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑋 ∈ Fin ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
23 22 3com23 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )