Metamath Proof Explorer

Theorem odf1o1

Description: An element with zero order has infinitely many multiples. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odf1o1.x 
|- X = ( Base ` G )
odf1o1.t 
|- .x. = ( .g ` G )
odf1o1.o 
|- O = ( od ` G )
odf1o1.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion odf1o1 
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x .x. A ) ) : ZZ -1-1-onto-> ( K ` { A } ) )

Proof

Step Hyp Ref Expression
1 odf1o1.x 
 |-  X = ( Base ` G )
2 odf1o1.t 
 |-  .x. = ( .g ` G )
3 odf1o1.o 
 |-  O = ( od ` G )
4 odf1o1.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
5 simpl1 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> G e. Grp )
6 1 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` X ) )
7 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` X ) -> ( SubGrp ` G ) e. ( Moore ` X ) )
8 5 6 7 3syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> ( SubGrp ` G ) e. ( Moore ` X ) )
9 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> A e. X )
10 9 snssd 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> { A } C_ X )
11 4 mrccl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` X ) /\ { A } C_ X ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
12 8 10 11 syl2anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
13 simpr 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> x e. ZZ )
14 8 4 10 mrcssidd 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> { A } C_ ( K ` { A } ) )
15 snidg 
 |-  ( A e. X -> A e. { A } )
16 9 15 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> A e. { A } )
17 14 16 sseldd 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> A e. ( K ` { A } ) )
18 2 subgmulgcl 
 |-  ( ( ( K ` { A } ) e. ( SubGrp ` G ) /\ x e. ZZ /\ A e. ( K ` { A } ) ) -> ( x .x. A ) e. ( K ` { A } ) )
19 12 13 17 18 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ x e. ZZ ) -> ( x .x. A ) e. ( K ` { A } ) )
20 19 ex 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ -> ( x .x. A ) e. ( K ` { A } ) ) )
21 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( O ` A ) = 0 )
22 21 breq1d 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( O ` A ) || ( x - y ) <-> 0 || ( x - y ) ) )
23 zsubcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x - y ) e. ZZ )
24 23 adantl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x - y ) e. ZZ )
25 0dvds 
 |-  ( ( x - y ) e. ZZ -> ( 0 || ( x - y ) <-> ( x - y ) = 0 ) )
26 24 25 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( 0 || ( x - y ) <-> ( x - y ) = 0 ) )
27 22 26 bitrd 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( O ` A ) || ( x - y ) <-> ( x - y ) = 0 ) )
28 simpl1 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> G e. Grp )
29 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A e. X )
30 simprl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ )
31 simprr 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ )
32 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
33 1 3 2 32 odcong 
 |-  ( ( G e. Grp /\ A e. X /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( O ` A ) || ( x - y ) <-> ( x .x. A ) = ( y .x. A ) ) )
34 28 29 30 31 33 syl112anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( O ` A ) || ( x - y ) <-> ( x .x. A ) = ( y .x. A ) ) )
35 zcn 
 |-  ( x e. ZZ -> x e. CC )
36 zcn 
 |-  ( y e. ZZ -> y e. CC )
37 subeq0 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( x - y ) = 0 <-> x = y ) )
38 35 36 37 syl2an 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x - y ) = 0 <-> x = y ) )
39 38 adantl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x - y ) = 0 <-> x = y ) )
40 27 34 39 3bitr3d 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x .x. A ) = ( y .x. A ) <-> x = y ) )
41 40 ex 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x .x. A ) = ( y .x. A ) <-> x = y ) ) )
42 20 41 dom2lem 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x .x. A ) ) : ZZ -1-1-> ( K ` { A } ) )
43 19 fmpttd 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x .x. A ) ) : ZZ --> ( K ` { A } ) )
44 eqid 
 |-  ( x e. ZZ |-> ( x .x. A ) ) = ( x e. ZZ |-> ( x .x. A ) )
45 1 2 44 4 cycsubg2 
 |-  ( ( G e. Grp /\ A e. X ) -> ( K ` { A } ) = ran ( x e. ZZ |-> ( x .x. A ) ) )
46 45 3adant3 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( K ` { A } ) = ran ( x e. ZZ |-> ( x .x. A ) ) )
47 46 eqcomd 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ran ( x e. ZZ |-> ( x .x. A ) ) = ( K ` { A } ) )
48 dffo2 
 |-  ( ( x e. ZZ |-> ( x .x. A ) ) : ZZ -onto-> ( K ` { A } ) <-> ( ( x e. ZZ |-> ( x .x. A ) ) : ZZ --> ( K ` { A } ) /\ ran ( x e. ZZ |-> ( x .x. A ) ) = ( K ` { A } ) ) )
49 43 47 48 sylanbrc 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x .x. A ) ) : ZZ -onto-> ( K ` { A } ) )
50 df-f1o 
 |-  ( ( x e. ZZ |-> ( x .x. A ) ) : ZZ -1-1-onto-> ( K ` { A } ) <-> ( ( x e. ZZ |-> ( x .x. A ) ) : ZZ -1-1-> ( K ` { A } ) /\ ( x e. ZZ |-> ( x .x. A ) ) : ZZ -onto-> ( K ` { A } ) ) )
51 42 49 50 sylanbrc 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x .x. A ) ) : ZZ -1-1-onto-> ( K ` { A } ) )