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 ⊢ X = Base G
odcl2.2 ⊢ O = od ⁡ G
Assertion oddvds2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → O ⁡ A ∥ X

Proof

Step Hyp Ref Expression
1 odcl2.1 ⊢ X = Base G
2 odcl2.2 ⊢ O = od ⁡ G
3 eqid ⊢ ⋅ G = ⋅ G
4 eqid ⊢ x ∈ ℤ ⟼ x ⋅ G A = x ∈ ℤ ⟼ x ⋅ G A
5 1 2 3 4 dfod2 ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A = if ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin ran ⁡ x ∈ ℤ ⟼ x ⋅ G A 0
6 5 3adant2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → O ⁡ A = if ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin ran ⁡ x ∈ ℤ ⟼ x ⋅ G A 0
7 simp2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → X ∈ Fin
8 1 3 4 cycsubgcl ⊢ G ∈ Grp ∧ A ∈ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ SubGrp ⁡ G ∧ A ∈ ran ⁡ x ∈ ℤ ⟼ x ⋅ G A
9 8 3adant2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ SubGrp ⁡ G ∧ A ∈ ran ⁡ x ∈ ℤ ⟼ x ⋅ G A
10 9 simpld ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ SubGrp ⁡ G
11 1 subgss ⊢ ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ SubGrp ⁡ G → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ⊆ X
12 10 11 syl ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ⊆ X
13 7 12 ssfid ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin
14 13 iftrued ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → if ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin ran ⁡ x ∈ ℤ ⟼ x ⋅ G A 0 = ran ⁡ x ∈ ℤ ⟼ x ⋅ G A
15 6 14 eqtrd ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → O ⁡ A = ran ⁡ x ∈ ℤ ⟼ x ⋅ G A
16 1 lagsubg ⊢ ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ SubGrp ⁡ G ∧ X ∈ Fin → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∥ X
17 10 7 16 syl2anc ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∥ X
18 15 17 eqbrtrd ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → O ⁡ A ∥ X