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=BaseG
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=BaseG
2 odcl2.2 ⊢O=od⁡G
3 eqid ⊢⋅G=⋅G
4 eqid ⊢x∈ℤ⟼x⋅GA=x∈ℤ⟼x⋅GA
5 1 2 3 4 dfod2 ⊢G∈Grp∧A∈X→O⁡A=ifran⁡x∈ℤ⟼x⋅GA∈Finran⁡x∈ℤ⟼x⋅GA0
6 5 3adant2 ⊢G∈Grp∧X∈Fin∧A∈X→O⁡A=ifran⁡x∈ℤ⟼x⋅GA∈Finran⁡x∈ℤ⟼x⋅GA0
7 simp2 ⊢G∈Grp∧X∈Fin∧A∈X→X∈Fin
8 1 3 4 cycsubgcl ⊢G∈Grp∧A∈X→ran⁡x∈ℤ⟼x⋅GA∈SubGrp⁡G∧A∈ran⁡x∈ℤ⟼x⋅GA
9 8 3adant2 ⊢G∈Grp∧X∈Fin∧A∈X→ran⁡x∈ℤ⟼x⋅GA∈SubGrp⁡G∧A∈ran⁡x∈ℤ⟼x⋅GA
10 9 simpld ⊢G∈Grp∧X∈Fin∧A∈X→ran⁡x∈ℤ⟼x⋅GA∈SubGrp⁡G
11 1 subgss ⊢ran⁡x∈ℤ⟼x⋅GA∈SubGrp⁡G→ran⁡x∈ℤ⟼x⋅GA⊆X
12 10 11 syl ⊢G∈Grp∧X∈Fin∧A∈X→ran⁡x∈ℤ⟼x⋅GA⊆X
13 7 12 ssfid ⊢G∈Grp∧X∈Fin∧A∈X→ran⁡x∈ℤ⟼x⋅GA∈Fin
14 13 iftrued ⊢G∈Grp∧X∈Fin∧A∈X→ifran⁡x∈ℤ⟼x⋅GA∈Finran⁡x∈ℤ⟼x⋅GA0=ran⁡x∈ℤ⟼x⋅GA
15 6 14 eqtrd ⊢G∈Grp∧X∈Fin∧A∈X→O⁡A=ran⁡x∈ℤ⟼x⋅GA
16 1 lagsubg ⊢ran⁡x∈ℤ⟼x⋅GA∈SubGrp⁡G∧X∈Fin→ran⁡x∈ℤ⟼x⋅GA∥X
17 10 7 16 syl2anc ⊢G∈Grp∧X∈Fin∧A∈X→ran⁡x∈ℤ⟼x⋅GA∥X
18 15 17 eqbrtrd ⊢G∈Grp∧X∈Fin∧A∈X→O⁡A∥X