Metamath Proof Explorer

Theorem odf1

Description: The multiples of an element with infinite order form an infinite cyclic subgroup of G . (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odf1.1 
|- X = ( Base ` G )
odf1.2 
|- O = ( od ` G )
odf1.3 
|- .x. = ( .g ` G )
odf1.4 
|- F = ( x e. ZZ |-> ( x .x. A ) )
Assertion odf1 
|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 <-> F : ZZ -1-1-> X ) )

Proof

Step Hyp Ref Expression
1 odf1.1 
 |-  X = ( Base ` G )
2 odf1.2 
 |-  O = ( od ` G )
3 odf1.3 
 |-  .x. = ( .g ` G )
4 odf1.4 
 |-  F = ( x e. ZZ |-> ( x .x. A ) )
5 1 3 mulgcl 
 |-  ( ( G e. Grp /\ x e. ZZ /\ A e. X ) -> ( x .x. A ) e. X )
6 5 3expa 
 |-  ( ( ( G e. Grp /\ x e. ZZ ) /\ A e. X ) -> ( x .x. A ) e. X )
7 6 an32s 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ x e. ZZ ) -> ( x .x. A ) e. X )
8 7 4 fmptd 
 |-  ( ( G e. Grp /\ A e. X ) -> F : ZZ --> X )
9 8 adantr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) -> F : ZZ --> X )
10 oveq1 
 |-  ( x = y -> ( x .x. A ) = ( y .x. A ) )
11 ovex 
 |-  ( x .x. A ) e. _V
12 10 4 11 fvmpt3i 
 |-  ( y e. ZZ -> ( F ` y ) = ( y .x. A ) )
13 oveq1 
 |-  ( x = z -> ( x .x. A ) = ( z .x. A ) )
14 13 4 11 fvmpt3i 
 |-  ( z e. ZZ -> ( F ` z ) = ( z .x. A ) )
15 12 14 eqeqan12d 
 |-  ( ( y e. ZZ /\ z e. ZZ ) -> ( ( F ` y ) = ( F ` z ) <-> ( y .x. A ) = ( z .x. A ) ) )
16 15 adantl 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( F ` y ) = ( F ` z ) <-> ( y .x. A ) = ( z .x. A ) ) )
17 simplr 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( O ` A ) = 0 )
18 17 breq1d 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( O ` A ) || ( y - z ) <-> 0 || ( y - z ) ) )
19 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
20 1 2 3 19 odcong 
 |-  ( ( G e. Grp /\ A e. X /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( O ` A ) || ( y - z ) <-> ( y .x. A ) = ( z .x. A ) ) )
21 20 ad4ant124 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( O ` A ) || ( y - z ) <-> ( y .x. A ) = ( z .x. A ) ) )
22 zsubcl 
 |-  ( ( y e. ZZ /\ z e. ZZ ) -> ( y - z ) e. ZZ )
23 22 adantl 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( y - z ) e. ZZ )
24 0dvds 
 |-  ( ( y - z ) e. ZZ -> ( 0 || ( y - z ) <-> ( y - z ) = 0 ) )
25 23 24 syl 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( 0 || ( y - z ) <-> ( y - z ) = 0 ) )
26 18 21 25 3bitr3d 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( y .x. A ) = ( z .x. A ) <-> ( y - z ) = 0 ) )
27 zcn 
 |-  ( y e. ZZ -> y e. CC )
28 zcn 
 |-  ( z e. ZZ -> z e. CC )
29 subeq0 
 |-  ( ( y e. CC /\ z e. CC ) -> ( ( y - z ) = 0 <-> y = z ) )
30 27 28 29 syl2an 
 |-  ( ( y e. ZZ /\ z e. ZZ ) -> ( ( y - z ) = 0 <-> y = z ) )
31 30 adantl 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( y - z ) = 0 <-> y = z ) )
32 16 26 31 3bitrd 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( F ` y ) = ( F ` z ) <-> y = z ) )
33 32 biimpd 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
34 33 ralrimivva 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) -> A. y e. ZZ A. z e. ZZ ( ( F ` y ) = ( F ` z ) -> y = z ) )
35 dff13 
 |-  ( F : ZZ -1-1-> X <-> ( F : ZZ --> X /\ A. y e. ZZ A. z e. ZZ ( ( F ` y ) = ( F ` z ) -> y = z ) ) )
36 9 34 35 sylanbrc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) -> F : ZZ -1-1-> X )
37 1 2 3 19 odid 
 |-  ( A e. X -> ( ( O ` A ) .x. A ) = ( 0g ` G ) )
38 1 19 3 mulg0 
 |-  ( A e. X -> ( 0 .x. A ) = ( 0g ` G ) )
39 37 38 eqtr4d 
 |-  ( A e. X -> ( ( O ` A ) .x. A ) = ( 0 .x. A ) )
40 39 ad2antlr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( ( O ` A ) .x. A ) = ( 0 .x. A ) )
41 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
42 41 ad2antlr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( O ` A ) e. NN0 )
43 42 nn0zd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( O ` A ) e. ZZ )
44 oveq1 
 |-  ( x = ( O ` A ) -> ( x .x. A ) = ( ( O ` A ) .x. A ) )
45 44 4 11 fvmpt3i 
 |-  ( ( O ` A ) e. ZZ -> ( F ` ( O ` A ) ) = ( ( O ` A ) .x. A ) )
46 43 45 syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( F ` ( O ` A ) ) = ( ( O ` A ) .x. A ) )
47 0zd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> 0 e. ZZ )
48 oveq1 
 |-  ( x = 0 -> ( x .x. A ) = ( 0 .x. A ) )
49 48 4 11 fvmpt3i 
 |-  ( 0 e. ZZ -> ( F ` 0 ) = ( 0 .x. A ) )
50 47 49 syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( F ` 0 ) = ( 0 .x. A ) )
51 40 46 50 3eqtr4d 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( F ` ( O ` A ) ) = ( F ` 0 ) )
52 simpr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> F : ZZ -1-1-> X )
53 f1fveq 
 |-  ( ( F : ZZ -1-1-> X /\ ( ( O ` A ) e. ZZ /\ 0 e. ZZ ) ) -> ( ( F ` ( O ` A ) ) = ( F ` 0 ) <-> ( O ` A ) = 0 ) )
54 52 43 47 53 syl12anc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( ( F ` ( O ` A ) ) = ( F ` 0 ) <-> ( O ` A ) = 0 ) )
55 51 54 mpbid 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ F : ZZ -1-1-> X ) -> ( O ` A ) = 0 )
56 36 55 impbida 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 <-> F : ZZ -1-1-> X ) )