Metamath Proof Explorer

Theorem odmulgid

Description: A relationship between the order of a multiple and the order of the basepoint. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odmulgid.1 
|- X = ( Base ` G )
odmulgid.2 
|- O = ( od ` G )
odmulgid.3 
|- .x. = ( .g ` G )
Assertion odmulgid 
|- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( O ` ( N .x. A ) ) || K <-> ( O ` A ) || ( K x. N ) ) )

Proof

Step Hyp Ref Expression
1 odmulgid.1 
 |-  X = ( Base ` G )
2 odmulgid.2 
 |-  O = ( od ` G )
3 odmulgid.3 
 |-  .x. = ( .g ` G )
4 simpl1 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> G e. Grp )
5 simpr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> K e. ZZ )
6 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> N e. ZZ )
7 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> A e. X )
8 1 3 mulgass 
 |-  ( ( G e. Grp /\ ( K e. ZZ /\ N e. ZZ /\ A e. X ) ) -> ( ( K x. N ) .x. A ) = ( K .x. ( N .x. A ) ) )
9 4 5 6 7 8 syl13anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( K x. N ) .x. A ) = ( K .x. ( N .x. A ) ) )
10 9 eqeq1d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( ( K x. N ) .x. A ) = ( 0g ` G ) <-> ( K .x. ( N .x. A ) ) = ( 0g ` G ) ) )
11 5 6 zmulcld 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( K x. N ) e. ZZ )
12 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
13 1 2 3 12 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ ( K x. N ) e. ZZ ) -> ( ( O ` A ) || ( K x. N ) <-> ( ( K x. N ) .x. A ) = ( 0g ` G ) ) )
14 4 7 11 13 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( O ` A ) || ( K x. N ) <-> ( ( K x. N ) .x. A ) = ( 0g ` G ) ) )
15 1 3 mulgcl 
 |-  ( ( G e. Grp /\ N e. ZZ /\ A e. X ) -> ( N .x. A ) e. X )
16 4 6 7 15 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( N .x. A ) e. X )
17 1 2 3 12 oddvds 
 |-  ( ( G e. Grp /\ ( N .x. A ) e. X /\ K e. ZZ ) -> ( ( O ` ( N .x. A ) ) || K <-> ( K .x. ( N .x. A ) ) = ( 0g ` G ) ) )
18 4 16 5 17 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( O ` ( N .x. A ) ) || K <-> ( K .x. ( N .x. A ) ) = ( 0g ` G ) ) )
19 10 14 18 3bitr4rd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( O ` ( N .x. A ) ) || K <-> ( O ` A ) || ( K x. N ) ) )