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

Metamath Proof Explorer

Theorem oddvds2

Description: The order of an element of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 14-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 odcl2.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl2.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
4 eqid ⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) )
5 1 2 3 4 dfod2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = if ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) , 0 ) )
6 5 3adant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = if ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) , 0 ) )
7 simp2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → 𝑋 ∈ Fin )
8 1 3 4 cycsubgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) )
9 8 3adant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) )
10 9 simpld ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
11 1 subgss ⊢ ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 )
12 10 11 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 )
13 7 12 ssfid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin )
14 13 iftrued ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → if ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) , 0 ) = ( ♯ ‘ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) )
15 6 14 eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = ( ♯ ‘ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) )
16 1 lagsubg ⊢ ( ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) ∥ ( ♯ ‘ 𝑋 ) )
17 10 7 16 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( ♯ ‘ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ) ∥ ( ♯ ‘ 𝑋 ) )
18 15 17 eqbrtrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑋 ) )