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 ) )