Metamath Proof Explorer

Theorem dfod2

Description: An alternative definition of the order of a group element is as the cardinality of the cyclic subgroup generated by the element. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 2-Oct-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 dfod2 
|- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = if ( ran F e. Fin , ( # ` ran F ) , 0 ) )

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 fzfid 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( 0 ... ( ( O ` A ) - 1 ) ) e. Fin )
6 1 3 mulgcl 
 |-  ( ( G e. Grp /\ x e. ZZ /\ A e. X ) -> ( x .x. A ) e. X )
7 6 3expa 
 |-  ( ( ( G e. Grp /\ x e. ZZ ) /\ A e. X ) -> ( x .x. A ) e. X )
8 7 an32s 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ x e. ZZ ) -> ( x .x. A ) e. X )
9 8 adantlr 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) -> ( x .x. A ) e. X )
10 9 4 fmptd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> F : ZZ --> X )
11 frn 
 |-  ( F : ZZ --> X -> ran F C_ X )
12 1 fvexi 
 |-  X e. _V
13 12 ssex 
 |-  ( ran F C_ X -> ran F e. _V )
14 10 11 13 3syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ran F e. _V )
15 elfzelz 
 |-  ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) -> y e. ZZ )
16 15 adantl 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> y e. ZZ )
17 ovex 
 |-  ( y .x. A ) e. _V
18 oveq1 
 |-  ( x = y -> ( x .x. A ) = ( y .x. A ) )
19 4 18 elrnmpt1s 
 |-  ( ( y e. ZZ /\ ( y .x. A ) e. _V ) -> ( y .x. A ) e. ran F )
20 16 17 19 sylancl 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( y .x. A ) e. ran F )
21 20 ralrimiva 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> A. y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( y .x. A ) e. ran F )
22 zmodfz 
 |-  ( ( x e. ZZ /\ ( O ` A ) e. NN ) -> ( x mod ( O ` A ) ) e. ( 0 ... ( ( O ` A ) - 1 ) ) )
23 22 ancoms 
 |-  ( ( ( O ` A ) e. NN /\ x e. ZZ ) -> ( x mod ( O ` A ) ) e. ( 0 ... ( ( O ` A ) - 1 ) ) )
24 23 adantll 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) -> ( x mod ( O ` A ) ) e. ( 0 ... ( ( O ` A ) - 1 ) ) )
25 simpllr 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( O ` A ) e. NN )
26 simplr 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> x e. ZZ )
27 15 adantl 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> y e. ZZ )
28 moddvds 
 |-  ( ( ( O ` A ) e. NN /\ x e. ZZ /\ y e. ZZ ) -> ( ( x mod ( O ` A ) ) = ( y mod ( O ` A ) ) <-> ( O ` A ) || ( x - y ) ) )
29 25 26 27 28 syl3anc 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( ( x mod ( O ` A ) ) = ( y mod ( O ` A ) ) <-> ( O ` A ) || ( x - y ) ) )
30 27 zred 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> y e. RR )
31 25 nnrpd 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( O ` A ) e. RR+ )
32 0z 
 |-  0 e. ZZ
33 nnz 
 |-  ( ( O ` A ) e. NN -> ( O ` A ) e. ZZ )
34 33 adantl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. ZZ )
35 34 adantr 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) -> ( O ` A ) e. ZZ )
36 elfzm11 
 |-  ( ( 0 e. ZZ /\ ( O ` A ) e. ZZ ) -> ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) <-> ( y e. ZZ /\ 0 <_ y /\ y < ( O ` A ) ) ) )
37 32 35 36 sylancr 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) -> ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) <-> ( y e. ZZ /\ 0 <_ y /\ y < ( O ` A ) ) ) )
38 37 biimpa 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( y e. ZZ /\ 0 <_ y /\ y < ( O ` A ) ) )
39 38 simp2d 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> 0 <_ y )
40 38 simp3d 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> y < ( O ` A ) )
41 modid 
 |-  ( ( ( y e. RR /\ ( O ` A ) e. RR+ ) /\ ( 0 <_ y /\ y < ( O ` A ) ) ) -> ( y mod ( O ` A ) ) = y )
42 30 31 39 40 41 syl22anc 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( y mod ( O ` A ) ) = y )
43 42 eqeq2d 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( ( x mod ( O ` A ) ) = ( y mod ( O ` A ) ) <-> ( x mod ( O ` A ) ) = y ) )
44 eqcom 
 |-  ( ( x mod ( O ` A ) ) = y <-> y = ( x mod ( O ` A ) ) )
45 43 44 bitrdi 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( ( x mod ( O ` A ) ) = ( y mod ( O ` A ) ) <-> y = ( x mod ( O ` A ) ) ) )
46 simp-4l 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> G e. Grp )
47 simp-4r 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> A e. X )
48 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
49 1 2 3 48 odcong 
 |-  ( ( G e. Grp /\ A e. X /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( O ` A ) || ( x - y ) <-> ( x .x. A ) = ( y .x. A ) ) )
50 46 47 26 27 49 syl112anc 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( ( O ` A ) || ( x - y ) <-> ( x .x. A ) = ( y .x. A ) ) )
51 29 45 50 3bitr3rd 
 |-  ( ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) /\ y e. ( 0 ... ( ( O ` A ) - 1 ) ) ) -> ( ( x .x. A ) = ( y .x. A ) <-> y = ( x mod ( O ` A ) ) ) )
52 51 ralrimiva 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) -> A. y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( ( x .x. A ) = ( y .x. A ) <-> y = ( x mod ( O ` A ) ) ) )
53 reu6i 
 |-  ( ( ( x mod ( O ` A ) ) e. ( 0 ... ( ( O ` A ) - 1 ) ) /\ A. y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( ( x .x. A ) = ( y .x. A ) <-> y = ( x mod ( O ` A ) ) ) ) -> E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( x .x. A ) = ( y .x. A ) )
54 24 52 53 syl2anc 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) /\ x e. ZZ ) -> E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( x .x. A ) = ( y .x. A ) )
55 54 ralrimiva 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> A. x e. ZZ E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( x .x. A ) = ( y .x. A ) )
56 ovex 
 |-  ( x .x. A ) e. _V
57 56 rgenw 
 |-  A. x e. ZZ ( x .x. A ) e. _V
58 eqeq1 
 |-  ( z = ( x .x. A ) -> ( z = ( y .x. A ) <-> ( x .x. A ) = ( y .x. A ) ) )
59 58 reubidv 
 |-  ( z = ( x .x. A ) -> ( E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) z = ( y .x. A ) <-> E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( x .x. A ) = ( y .x. A ) ) )
60 4 59 ralrnmptw 
 |-  ( A. x e. ZZ ( x .x. A ) e. _V -> ( A. z e. ran F E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) z = ( y .x. A ) <-> A. x e. ZZ E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( x .x. A ) = ( y .x. A ) ) )
61 57 60 ax-mp 
 |-  ( A. z e. ran F E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) z = ( y .x. A ) <-> A. x e. ZZ E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( x .x. A ) = ( y .x. A ) )
62 55 61 sylibr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> A. z e. ran F E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) z = ( y .x. A ) )
63 eqid 
 |-  ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) |-> ( y .x. A ) ) = ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) |-> ( y .x. A ) )
64 63 f1ompt 
 |-  ( ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) |-> ( y .x. A ) ) : ( 0 ... ( ( O ` A ) - 1 ) ) -1-1-onto-> ran F <-> ( A. y e. ( 0 ... ( ( O ` A ) - 1 ) ) ( y .x. A ) e. ran F /\ A. z e. ran F E! y e. ( 0 ... ( ( O ` A ) - 1 ) ) z = ( y .x. A ) ) )
65 21 62 64 sylanbrc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) |-> ( y .x. A ) ) : ( 0 ... ( ( O ` A ) - 1 ) ) -1-1-onto-> ran F )
66 f1oen2g 
 |-  ( ( ( 0 ... ( ( O ` A ) - 1 ) ) e. Fin /\ ran F e. _V /\ ( y e. ( 0 ... ( ( O ` A ) - 1 ) ) |-> ( y .x. A ) ) : ( 0 ... ( ( O ` A ) - 1 ) ) -1-1-onto-> ran F ) -> ( 0 ... ( ( O ` A ) - 1 ) ) ~~ ran F )
67 5 14 65 66 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( 0 ... ( ( O ` A ) - 1 ) ) ~~ ran F )
68 enfi 
 |-  ( ( 0 ... ( ( O ` A ) - 1 ) ) ~~ ran F -> ( ( 0 ... ( ( O ` A ) - 1 ) ) e. Fin <-> ran F e. Fin ) )
69 67 68 syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( ( 0 ... ( ( O ` A ) - 1 ) ) e. Fin <-> ran F e. Fin ) )
70 5 69 mpbid 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ran F e. Fin )
71 70 iftrued 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> if ( ran F e. Fin , ( # ` ran F ) , 0 ) = ( # ` ran F ) )
72 fz01en 
 |-  ( ( O ` A ) e. ZZ -> ( 0 ... ( ( O ` A ) - 1 ) ) ~~ ( 1 ... ( O ` A ) ) )
73 ensym 
 |-  ( ( 0 ... ( ( O ` A ) - 1 ) ) ~~ ( 1 ... ( O ` A ) ) -> ( 1 ... ( O ` A ) ) ~~ ( 0 ... ( ( O ` A ) - 1 ) ) )
74 34 72 73 3syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( 1 ... ( O ` A ) ) ~~ ( 0 ... ( ( O ` A ) - 1 ) ) )
75 entr 
 |-  ( ( ( 1 ... ( O ` A ) ) ~~ ( 0 ... ( ( O ` A ) - 1 ) ) /\ ( 0 ... ( ( O ` A ) - 1 ) ) ~~ ran F ) -> ( 1 ... ( O ` A ) ) ~~ ran F )
76 74 67 75 syl2anc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( 1 ... ( O ` A ) ) ~~ ran F )
77 fzfid 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( 1 ... ( O ` A ) ) e. Fin )
78 hashen 
 |-  ( ( ( 1 ... ( O ` A ) ) e. Fin /\ ran F e. Fin ) -> ( ( # ` ( 1 ... ( O ` A ) ) ) = ( # ` ran F ) <-> ( 1 ... ( O ` A ) ) ~~ ran F ) )
79 77 70 78 syl2anc 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( ( # ` ( 1 ... ( O ` A ) ) ) = ( # ` ran F ) <-> ( 1 ... ( O ` A ) ) ~~ ran F ) )
80 76 79 mpbird 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( # ` ( 1 ... ( O ` A ) ) ) = ( # ` ran F ) )
81 nnnn0 
 |-  ( ( O ` A ) e. NN -> ( O ` A ) e. NN0 )
82 81 adantl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. NN0 )
83 hashfz1 
 |-  ( ( O ` A ) e. NN0 -> ( # ` ( 1 ... ( O ` A ) ) ) = ( O ` A ) )
84 82 83 syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( # ` ( 1 ... ( O ` A ) ) ) = ( O ` A ) )
85 71 80 84 3eqtr2rd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) e. NN ) -> ( O ` A ) = if ( ran F e. Fin , ( # ` ran F ) , 0 ) )
86 simp3 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( O ` A ) = 0 )
87 1 2 3 4 odinf 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran F e. Fin )
88 87 iffalsed 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> if ( ran F e. Fin , ( # ` ran F ) , 0 ) = 0 )
89 86 88 eqtr4d 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( O ` A ) = if ( ran F e. Fin , ( # ` ran F ) , 0 ) )
90 89 3expa 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( O ` A ) = 0 ) -> ( O ` A ) = if ( ran F e. Fin , ( # ` ran F ) , 0 ) )
91 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
92 91 adantl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) e. NN0 )
93 elnn0 
 |-  ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
94 92 93 sylib 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
95 85 90 94 mpjaodan 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = if ( ran F e. Fin , ( # ` ran F ) , 0 ) )