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 
|- X = ( Base ` G )
odcl2.2 
|- O = ( od ` G )
Assertion oddvds2 
|- ( ( G e. Grp /\ X e. Fin /\ A e. 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 ) = ( .g ` G )
4 eqid 
 |-  ( x e. ZZ |-> ( x ( .g ` G ) A ) ) = ( x e. ZZ |-> ( x ( .g ` G ) A ) )
5 1 2 3 4 dfod2 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = if ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin , ( # ` ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) , 0 ) )
6 5 3adant2 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( O ` A ) = if ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin , ( # ` ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) , 0 ) )
7 simp2 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> X e. Fin )
8 1 3 4 cycsubgcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. ( SubGrp ` G ) /\ A e. ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) )
9 8 3adant2 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. ( SubGrp ` G ) /\ A e. ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) )
10 9 simpld 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. ( SubGrp ` G ) )
11 1 subgss 
 |-  ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. ( SubGrp ` G ) -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) C_ X )
12 10 11 syl 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) C_ X )
13 7 12 ssfid 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin )
14 13 iftrued 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> if ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. Fin , ( # ` ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) , 0 ) = ( # ` ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) )
15 6 14 eqtrd 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( O ` A ) = ( # ` ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) )
16 1 lagsubg 
 |-  ( ( ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) || ( # ` X ) )
17 10 7 16 syl2anc 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( # ` ran ( x e. ZZ |-> ( x ( .g ` G ) A ) ) ) || ( # ` X ) )
18 15 17 eqbrtrd 
 |-  ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( O ` A ) || ( # ` X ) )